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

Metamath Proof Explorer

Theorem mpbiran

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996)

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

Proof

Step Hyp Ref Expression
1 mpbiran.1 ⊢ ψ
2 mpbiran.2 ⊢ φ ↔ ψ ∧ χ
3 1 biantrur ⊢ χ ↔ ψ ∧ χ
4 2 3 bitr4i ⊢ φ ↔ χ