Theorem baibd 948

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  pw2f1olem  8064  eluz  11701  elicc4  12240  s111  13395  limsupgle  14208  lo1resb  14295  o1resb  14297  isercolllem2  14396  divalgmodcl  15131  ismri2  16292  acsfiel2  16316  issect2  16414  eqglact  17645  eqgid  17646  cntzel  17756  dprdsubg  18423  subgdmdprd  18433  dprd2da  18441  dmdprdpr  18448  issubrg3  18808  ishil2  20063  obslbs  20074  iscld2  20832  isperf3  20957  cncnp2  21085  cnnei  21086  trfbas2  21647  flimrest  21787  flfnei  21795  fclsrest  21828  tsmssubm  21946  isnghm2  22528  isnghm3  22529  isnmhm2  22556  iscfil2  23064  caucfil  23081  ellimc2  23641  cnlimc  23652  lhop1  23777  dvfsumlem1  23789  fsumharmonic  24738  fsumvma  24938  fsumvma2  24939  vmasum  24941  chpchtsum  24944  chpub  24945  rpvmasum2  25201  dchrisum0lem1  25205  dirith  25218  uvtx2vtx1edg  26299  uvtx2vtx1edgb  26300  iscplgrnb  26312  frgr3v  27139  adjeu  28748  suppss3  29502  nndiffz1  29548  fsumcvg4  29996  qqhval2lem  30025  indpreima  30087  eulerpartlemf  30432  elorvc  30521  hashreprin  30698  neibastop3  32357  relowlpssretop  33212  sstotbnd2  33573  isbnd3b  33584  lshpkr  34404  isat2  34574  islln4  34793  islpln4  34817  islvol4  34860  islhp2  35283  pw2f1o2val2  37607  rfcnpre1  39178  rfcnpre2  39190