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

Metamath Proof Explorer

Theorem bimsc1

Description: Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion bimsc1 ⊢ φ → ψ ∧ χ ↔ ψ ∧ φ → χ ↔ φ

Proof

Step Hyp Ref Expression
1 id ⊢ χ ↔ ψ ∧ φ → χ ↔ ψ ∧ φ
2 simpr ⊢ ψ ∧ φ → φ
3 ancr ⊢ φ → ψ → φ → ψ ∧ φ
4 2 3 impbid2 ⊢ φ → ψ → ψ ∧ φ ↔ φ
5 1 4 sylan9bbr ⊢ φ → ψ ∧ χ ↔ ψ ∧ φ → χ ↔ φ