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

Metamath Proof Explorer

Theorem mpbir2an

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005)

Ref Expression
Hypotheses mpbir2an.1 ⊢ ψ
mpbir2an.2 ⊢ χ
mpbir2an.maj ⊢ φ ↔ ψ ∧ χ
Assertion mpbir2an ⊢ φ

Proof

Step Hyp Ref Expression
1 mpbir2an.1 ⊢ ψ
2 mpbir2an.2 ⊢ χ
3 mpbir2an.maj ⊢ φ ↔ ψ ∧ χ
4 1 3 mpbiran ⊢ φ ↔ χ
5 2 4 mpbir ⊢ φ