Theorem sylib 198

Description: A mixed syllogism inference from an implication and a biconditional.

Hypotheses

Ref	Expression
sylib.1	|- (ph -> ps)
sylib.2	|- (ps <-> ch)

Assertion

Ref	Expression
sylib	|- (ph -> ch)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 |- (ph -> ps)
2		sylib.2	. . 3 |- (ps <-> ch)
3	2	biimp 151	. 2 |- (ps -> ch)
4	1, 3	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3imtr3 218  ord 232  exp3a 375  imdistand 445  bicomd 521  pm2.85 579  pm5.74d 585  mpbidi 589  negbid 611  pm4.71rd 639  pm5.32d 647  pm5.18 660  ecase2d 751  consensus 767  3mix3 817  ecase23d 922  excomim 1045  19.23ai 1064  19.23ad 1066  nexd 1102  sbf 1186  hbs1f 1189  sbied 1195  sbequi 1228  sbn 1231  a4sbe 1243  a4sbim 1244  a4sbbi 1245  sb6rf 1260  sb8 1261  sb9i 1263  eu2 1396  mooran1 1425  euor2 1437  2eu1 1449  eqcomd 1480  necon2bi 1612  necon2i 1613  necon4i 1625  necomd 1637  r19.21bi 1725  nrexdv 1730  elex 1819  ceqsalg 1825  cla4gf 1860  3sstr3g 2101  syl6ss 2107  sseq0 2304  un00 2306  npss0 2309  disjpss 2319  ssnelpss 2330  pssnel 2331  difsnid 2467  sneqr 2477  preqr1 2481  preq12b 2483  ssiun 2592  iununi 2616  3brtr3g 2646  axrep1 2694  axrep2 2695  axrep4 2697  axrep5 2698  class2set 2734  0inp0 2738  pwel 2759  exss 2769  opth1 2786  opthwiener 2807  pwssun 2827  sotric 2860  difex2 2877  euuni 2881  reucl 2885  reuxfr2 2903  reuhyp 2905  iunpw 2914  efrn2lp 2929  epne3 2930  dfwe2 2935  wecmpep 2941  wereu 2945  ordtri3or 2979  ordtri1 2980  ordtri3 2983  ordeleqon 2990  sucexg 3049  suceloni 3062  ordnbtwn 3063  orddif 3075  orduniss 3076  ordtri2or 3077  ordunisuc 3089  suc11 3093  onelin 3103  onelun 3104  onuninsuc 3108  ordunisuc2 3115  dflim3 3118  limsssuc 3121  on0eqelt 3124  tfi 3126  find 3155  finds2 3158  tfindsg2 3163  ssrel 3247  elrel 3253  xpsspw 3257  relop 3275  opelxpex2 3279  dmxp 3332  resopab2 3398  relimasn 3425  ndmima 3434  funopg 3547  funun 3554  funcnvuni 3564  funin 3566  funcnvres2 3570  imadif 3574  fneu2 3593  fn0 3605  fnopabg 3615  fcoi2 3646  fcnvres 3648  f00 3657  foconst 3683  f1ococnv2 3708  f1ococnv1 3709  fvprc 3721  fv3 3733  tz6.12-2 3739  fvopabn 3786  elrnopabg 3800  exfo 3822  fopab2 3823  fsn 3834  fnressn 3837  tfrlem5 3915  tfrlem8 3918  tz7.48-2 3957  abianfp 3962  funoprabg 4010  curry1 4098  curry1f 4099  1stcof 4101  elrnoprabg 4124  oalimcl 4194  omlimcl 4209  brecop2 4307  ecopoprdm 4309  mapsn 4345  ixp0 4361  en2d 4400  dom2d 4404  fundmen 4428  unen 4434  pw2en 4446  sbthlem3 4449  sbthlem4 4450  sbthlem5 4451  sbthlem6 4452  sdomdomtr 4469  fodomr 4483  xpen 4488  mapenlem2 4490  mapdom2 4494  mapxpen 4495  xpmapenlem3 4498  xpmapenlem5 4500  mapunen 4502  pwen 4503  ssenen 4504  nneneq 4512  php 4513  isfinite1OLD 4531  infn0 4533  ssfi 4537  ssfiOLD 4538  unblem2 4541  isfinite2OLD 4546  unfi 4551  unfiOLD 4552  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii2OLD 4562  pwfilemOLD 4570  zfregcl 4595  elirrv 4598  inf3lem3 4615  inf3lem6 4618  infeq5 4621  noinfep 4640  zfregs 4647  r1val1 4658  rankr1 4674  rankuni 4698  rankval4 4702  rankc2 4706  rankelun 4707  rankelpr 4708  rankelop 4709  rankxplim 4712  rankxplim3 4714  rankxpsuc 4715  hta 4728  aceq3lem 4732  aceq5lem4 4738  aceq5 4740  ac6lem 4754  ac9s 4764  kmlem1 4765  kmlem4 4768  kmlem5 4769  kmlem7 4771  kmlem11 4775  zorn2lem4 4791  zorn2lem6 4793  zorn 4797  fodomb 4800  brdom3 4801  brdom5 4802  brdom4 4803  imadomg 4806  cardmin 4860  cardprc 4861  alephnbtwn 4868  cardaleph 4885  alephval3 4903  cflem 4905  cfval 4906  cfeq0 4914  cdavalt 4919  nd1 4938  nd2 4939  axpownd 4953  zfcndext 4965  zfcndrep 4966  distrpq 5067  prn0 5093  prnmax 5099  genpn0 5106  genpnnp 5108  prlem934 5139  ltaddpr 5140  prlem936 5155  reclem2pr 5157  suplem1pr 5161  suppsr 5222  supsrlem6 5230  ltresr 5258  supre 5260  negeu 5355  lttri4t 5515  ltnsym2t 5533  renfdisj 5539  xrltnsym2t 5551  xrrebndt 5568  receu 5701  rec11i 5777  eqneg 5804  nnind 5937  nn1suc 5939  nnleltp1t 5954  nominpos 6043  lble 6047  bndndx 6073  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  supxrre 6083  elnnz 6145  elnnz1 6155  uzwo3 6218  icounlem 6412  snunioolem 6414  uzwo 6455  uzwoOLD 6456  nnwof 6459  elfzp1 6510  fzneuzt 6518  expnnvalt 6572  discrlem3 6658  nn0opthlem2 6665  nn0opth 6666  sqrlem13 6685  sqr2irrlem3 6726  crulem 6736  crne0 6739  creui 6743  replimt 6761  abssubne0t 6882  cvg1 6921  cvg2 6922  cvg3 6923  faclbnd4lem4 6951  dffsum 6998  serzfsum 7004  fsump1s 7013  fsum1ps 7018  fsumshft 7031  fsumcmp 7040  bcxmas 7076  clm3 7079  climreu 7101  climrecl 7110  climge0 7112  climubi 7153  dfisum 7191  infcvglem1 7221  infcvglem3 7223  cvgratlem5 7254  fsum0diag4 7261  cncffvrn 7273  abscncflem 7274  mulc1cncf 7279  ivthlem3 7283  ivthlem5 7285  ivthlem6 7286  ivthlem7 7287  efseq0ex 7311  efclt 7312  efcvg 7314  efcvgfsum 7315  reeftlclt 7380  eflt 7406  efcnlem1 7419  efcn 7423  sinbndt 7465  cosbndt 7466  acdc5lem1 7491  acdcALT 7496  unbenlem 7504  infxpidmlem7 7558  infxpidmlem8 7559  infxpidmlem10 7561  infxpidmlem11 7562  infxpidmlem12 7563  infpss 7574  iunctb 7575  basgen2t 7639  subbasOLD 7644  fctopOLD 7650  cctop 7652  clsval 7677  uncld 7681  ntrval2 7686  cmclsopn 7693  cmntrcld 7694  elcls 7704  neif 7715  0nnei 7726  islp2 7747  clslp 7748  qdensere 7751  idcn 7766  ismsg 7800  metreslem 7822  blf 7844  cncfmet 7905  lmuni 7951  lmsslem 7952  lmfexlem1 7956  metcnp4 7970  xplmi 7973  xpcn 7976  oprcn 7977  bopcnlem1 7981  bopcnlem4 7984  bcthlem4 8002  bcthlem7 8005  bcthlem9 8007  bcthlem14 8012  bcthlem28 8026  bcthlem29 8027  bcthlem30 8028  bcthlem31 8029  bcthlem33 8031  grpideu 8053  grprn 8056  isgrp2i 8076  grpinvf 8079  grpdivf 8085  resgrprn 8095  grplactf1o 8098  vcex 8199  nvvcop 8213  nvvop 8228  nvex 8230  nvmf 8266  sqcn 8335  va1cnlem 8345  ipf 8366  ip1cnilem2 8374  ip1cnilem3 8375  nmlno0lem 8453  siilem1 8511  ipblnfi 8516  ubthlem3 8531  minveclem26 8570  pilem1 8671  pilem2 8672  sinperlem2 8687  sincosq2sgn 8705  sincosq4sgn 8707  efifolem2 8723  efif1lem5 8734  efif1lem7 8736  grothinf 8781  axhcompl 8868  bcseq 8986  chcmh 9113  norm1ex 9122  shorth 9168  occllem4 9176  projlem24 9209  pjthlem11 9229  pjtheu2 9250  pjoc1 9264  spanvalt 9299  hsupval2t 9300  shlej1 9348  shs00 9373  chj00 9410  chabs2t 9440  h1de2 9476  cmbr4 9544  spansnm0 9595  nonbool 9596  5oalem5 9603  pjssm 9626  pjvect 9641  pjocvect 9642  hoaddclt 9684  homulclt 9685  eigpos 9762  dmadjopt 9820  brafnt 9871  kbopt 9877  nmlnop0ALT 9920  lnopeq0 9932  nmcopexlem4 9954  nmcfnexlem4 9983  cnlnadjlem2 10001  cnlnadjlem3 10002  cnlnadjlem4 10003  cnlnadjlem5 10004  cnlnssadj 10013  nmopco 10028  cnvbravalt 10043  kbass2t 10050  pjss1co 10091  pjss2co 10092  pjorthco 10097  pjscj 10098  pjssdif2 10102  pjssdif1 10103  pjclem4 10127  pjc 10128  pj3s 10135  pj3cor1 10137  strlem3a 10179  strlem6 10183  hstrlem3a 10187  hstrlem6 10191  mdbr3 10224  mdbr4 10225  dmdbr5 10235  ssmd2 10239  mdslj1 10246  mdslj2 10247  mdsl2b 10250  cvmd 10251  mdslmd1lem1 10252  mdslmd1lem2 10253  hatomistic 10289  chrelat2 10292  atssmat 10305  atoml2 10310  irredlem1 10317  irredlem2 10318  mdsymlem1 10330  mdsymlem2 10331  mdsymlem5 10334  dmdbr4at 10348  dmdbr5at 10349  ghomfo 10391  ghomgsg 10395  ghomf1olem 10396  cayleylem2 10410  faimpex 10438  esnnei 10508  cnvhmpha 10525  hmphsyma 10528  hmphre 10530  hmeogrp 10538  homcard 10539  fillsb 10560  fipfil2 10564  fipfil2OLD 10565  efilcp 10572  efilcpOLD 10573  filint2 10574  filint2OLD 10575  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  dtt2 10618  trdom 10635  cnvtr 10638  homib 10724  hgrablkne0 10773

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain