Metamath Proof Explorer


Theorem baib

Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999)

Ref Expression
Hypothesis baib.1 φ ψ χ
Assertion baib ψ φ χ

Proof

Step Hyp Ref Expression
1 baib.1 φ ψ χ
2 ibar ψ χ ψ χ
3 2 1 syl6rbbr ψ φ χ