This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ψ → φ ↔ χ