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:  pw2f1odclem  7138  2omap  7324  eluz  9951  elicc4  10359  s111  11421  divalgmodcl  12720  eqglact  14087  eqgid  14088  cntzel  14155  iscrng2  14426  issubrg3  14664  iscld2  15330  cncnp2m  15457  cnnei  15458  reopnap  15772  cnlimc  15898  pw1map  17230