Theorem baibd 907

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

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

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 369

This theorem is referenced by:  pw2f1olem  7614  eluz  11095  elicc4  11594  s111  12612  limsupgle  13382  lo1resb  13469  o1resb  13471  isercolllem2  13570  ismri2  15121  acsfiel2  15144  issect2  15242  eqglact  16451  eqgid  16452  cntzel  16560  dprdsubg  17266  subgdmdprd  17276  dprd2da  17286  dmdprdpr  17293  issubrg3  17652  ishil2  18923  obslbs  18934  iscld2  19696  isperf3  19821  cncnp2  19949  cnnei  19950  trfbas2  20510  flimrest  20650  flfnei  20658  fclsrest  20691  tsmssubm  20810  isnghm2  21397  isnghm3  21398  isnmhm2  21425  iscfil2  21871  caucfil  21888  ellimc2  22447  cnlimc  22458  lhop1  22581  dvfsumlem1  22593  fsumharmonic  23539  fsumvma  23686  fsumvma2  23687  vmasum  23689  chpchtsum  23692  chpub  23693  rpvmasum2  23895  dchrisum0lem1  23899  dirith  23912  cusgrauvtxb  24698  adjeu  27006  suppss3  27781  nndiffz1  27830  fsumcvg4  28167  qqhval2lem  28196  indpreima  28254  eulerpartlemf  28573  elorvc  28662  neibastop3  30420  sstotbnd2  30510  isbnd3b  30521  pw2f1o2val2  31221  rfcnpre1  31634  rfcnpre2  31646  lshpkr  35239  isat2  35409  islln4  35628  islpln4  35652  islvol4  35695  islhp2  36118