Theorem baibd 931

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 462	1 |- ( ( ph /\ ch ) -> ( ps <-> th ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pw2f1odclem  7063  eluz  9830  elicc4  10236  s111  11274  divalgmodcl  12569  eqglact  13892  eqgid  13893  iscrng2  14109  issubrg3  14342  iscld2  14915  cncnp2m  15042  cnnei  15043  reopnap  15357  cnlimc  15483  2omap  16715  pw1map  16717