Theorem baibd 900

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 504	. . 3 |- ( ch -> ( th <-> ( ch /\ th ) ) )
3	2	bicomd 201	. 2 |- ( ch -> ( ( ch /\ th ) <-> th ) )
4	1, 3	sylan9bb 699	1 |- ( ( ph /\ ch ) -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  pw2f1olem  7415  eluz  10874  elicc4  11362  s111  12302  limsupgle  12955  lo1resb  13042  o1resb  13044  isercolllem2  13143  ismri2  14570  acsfiel2  14593  issect2  14693  eqglact  15732  eqgid  15733  cntzel  15841  dprdsubg  16521  subgdmdprd  16531  dprd2da  16541  dmdprdpr  16548  issubrg3  16893  ishil2  18144  obslbs  18155  iscld2  18632  isperf3  18757  cncnp2  18885  cnnei  18886  trfbas2  19416  flimrest  19556  flfnei  19564  fclsrest  19597  tsmssubm  19716  isnghm2  20303  isnghm3  20304  isnmhm2  20331  iscfil2  20777  caucfil  20794  ellimc2  21352  cnlimc  21363  lhop1  21486  dvfsumlem1  21498  fsumharmonic  22405  fsumvma  22552  fsumvma2  22553  vmasum  22555  chpchtsum  22558  chpub  22559  rpvmasum2  22761  dchrisum0lem1  22765  dirith  22778  cusgrauvtxb  23404  adjeu  25293  suppss3  26027  nndiffz1  26075  fsumcvg4  26380  qqhval2lem  26410  indpreima  26481  eulerpartlemf  26753  elorvc  26842  neibastop3  28583  sstotbnd2  28673  isbnd3b  28684  pw2f1o2val2  29389  rfcnpre1  29741  rfcnpre2  29753  lshpkr  32762  isat2  32932  islln4  33151  islpln4  33175  islvol4  33218  islhp2  33641