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  7318  eluz  9935  elicc4  10342  s111  11399  divalgmodcl  12695  eqglact  14028  eqgid  14029  iscrng2  14319  issubrg3  14555  iscld2  15205  cncnp2m  15332  cnnei  15333  reopnap  15647  cnlimc  15773  pw1map  17025