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 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  7621  eluz  11094  elicc4  11590  s111  12585  limsupgle  13262  lo1resb  13349  o1resb  13351  isercolllem2  13450  ismri2  14886  acsfiel2  14909  issect2  15009  eqglact  16054  eqgid  16055  cntzel  16163  dprdsubg  16870  subgdmdprd  16880  dprd2da  16890  dmdprdpr  16897  issubrg3  17252  ishil2  18533  obslbs  18544  iscld2  19311  isperf3  19436  cncnp2  19564  cnnei  19565  trfbas2  20095  flimrest  20235  flfnei  20243  fclsrest  20276  tsmssubm  20395  isnghm2  20982  isnghm3  20983  isnmhm2  21010  iscfil2  21456  caucfil  21473  ellimc2  22032  cnlimc  22043  lhop1  22166  dvfsumlem1  22178  fsumharmonic  23085  fsumvma  23232  fsumvma2  23233  vmasum  23235  chpchtsum  23238  chpub  23239  rpvmasum2  23441  dchrisum0lem1  23445  dirith  23458  cusgrauvtxb  24188  adjeu  26500  suppss3  27238  nndiffz1  27280  fsumcvg4  27584  qqhval2lem  27614  indpreima  27694  eulerpartlemf  27965  elorvc  28054  neibastop3  29799  sstotbnd2  29889  isbnd3b  29900  pw2f1o2val2  30602  rfcnpre1  30988  rfcnpre2  31000  lshpkr  33923  isat2  34093  islln4  34312  islpln4  34336  islvol4  34379  islhp2  34802