Theorem baibd 920

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pw2f1olem  7663  eluz  11162  elicc4  11691  s111  12751  limsupgle  13546  lo1resb  13639  o1resb  13641  isercolllem2  13740  ismri2  15549  acsfiel2  15572  issect2  15670  eqglact  16879  eqgid  16880  cntzel  16988  dprdsubg  17668  subgdmdprd  17678  dprd2da  17686  dmdprdpr  17693  issubrg3  18047  ishil2  19293  obslbs  19304  iscld2  20054  isperf3  20180  cncnp2  20308  cnnei  20309  trfbas2  20869  flimrest  21009  flfnei  21017  fclsrest  21050  tsmssubm  21168  isnghm2  21740  isnghm3  21741  isnghm2OLD  21758  isnghm3OLD  21759  isnmhm2  21784  iscfil2  22247  caucfil  22264  ellimc2  22844  cnlimc  22855  lhop1  22978  dvfsumlem1  22990  fsumharmonic  23949  fsumvma  24153  fsumvma2  24154  vmasum  24156  chpchtsum  24159  chpub  24160  rpvmasum2  24362  dchrisum0lem1  24366  dirith  24379  cusgrauvtxb  25236  adjeu  27554  suppss3  28320  nndiffz1  28374  fsumcvg4  28763  qqhval2lem  28792  indpreima  28853  eulerpartlemf  29209  elorvc  29298  neibastop3  31024  relowlpssretop  31769  sstotbnd2  32108  isbnd3b  32119  lshpkr  32685  isat2  32855  islln4  33074  islpln4  33098  islvol4  33141  islhp2  33564  pw2f1o2val2  35897  rfcnpre1  37337  rfcnpre2  37349  uvtx2vtx1edg  39573  uvtx2vtx1edgb  39574  iscplgrnb  39586