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  7134  2omap  7319  eluz  9945  elicc4  10353  s111  11415  divalgmodcl  12714  eqglact  14081  eqgid  14082  cntzel  14149  iscrng2  14403  issubrg3  14639  iscld2  15296  cncnp2m  15423  cnnei  15424  reopnap  15738  cnlimc  15864  pw1map  17191