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 1 2 bitr4id ( 𝜓 → ( 𝜑𝜒 ) )