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 φ ψ χ ψ φ χ φ