Theorem baibd 935

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
baibd.1	|- ( ph -> ( ps <-> ( ch /\ th ) ) )

Assertion

Ref	Expression
baibd	|- ( ( ph /\ ch ) -> ( ps <-> th ) )

Proof of Theorem baibd

Step	Hyp	Ref	Expression
1		baibd.1	. 2 |- ( ph -> ( ps <-> ( ch /\ th ) ) )
2		ibar 301	. . 3 |- ( ch -> ( th <-> ( ch /\ th ) ) )
3	2	bicomd 141	. 2 |- ( ch -> ( ( ch /\ th ) <-> th ) )
4	1, 3	sylan9bb 466	1 |- ( ( ph /\ ch ) -> ( ps <-> th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  suppinisegdc  6513  pw2f1odclem  7140  2omap  7324  eluz  9950  elicc4  10358  s111  11420  divalgmodcl  12719  eqglact  14086  eqgid  14087  cntzel  14154  iscrng2  14425  issubrg3  14663  iscld2  15347  cncnp2m  15474  cnnei  15475  reopnap  15789  cnlimc  15915  pw1map  17247