Theorem bimsc1

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

	Ref	Expression
Assertion	bimsc1	|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( ch <-> ( ps /\ ph ) ) -> ( ch <-> ( ps /\ ph ) ) )
2		simpr	|- ( ( ps /\ ph ) -> ph )
3		ancr	|- ( ( ph -> ps ) -> ( ph -> ( ps /\ ph ) ) )
4	2 3	impbid2	|- ( ( ph -> ps ) -> ( ( ps /\ ph ) <-> ph ) )
5	1 4	sylan9bbr	|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )