Let A —> B be a local homomorphism of Noetherian local rings. Assume A —> B is formally smooth in the m_B-adic topology. Then A —> B is flat. See Tag 07NP.

PS: Of course much more is true, see Tag 07NQ.