Metamath Proof Explorer


Theorem baibd

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis baibd.1 φψχθ
Assertion baibd φχψθ

Proof

Step Hyp Ref Expression
1 baibd.1 φψχθ
2 ibar χθχθ
3 2 bicomd χχθθ
4 1 3 sylan9bb φχψθ