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 519  pm2.85 577  pm5.74d 583  mpbidi 587  negbid 609  pm4.71rd 637  pm5.32d 645  pm5.18 658  ecase2d 749  consensus 765  3mix3 815  ecase23d 919  excomim 1041  19.23ai 1060  19.23ad 1062  nexd 1098  sbf 1182  hbs1f 1185  sbied 1191  sbequi 1223  sbn 1226  a4sbe 1238  a4sbim 1239  a4sbbi 1240  sb6rf 1255  sb8 1256  sb9i 1258  eu2 1389  mooran1 1418  euor2 1430  2eu1 1442  eqcomd 1472  necon2bi 1604  necon2i 1605  necon4i 1617  necomd 1629  r19.21bi 1717  nrexdv 1722  elex 1810  ceqsalg 1816  cla4gf 1851  3sstr3g 2091  syl6ss 2097  sseq0 2294  un00 2296  npss0 2299  disjpss 2309  ssnelpss 2320  pssnel 2321  difsnid 2458  sneqr 2468  preqr1 2472  preq12b 2474  ssiun 2582  iununi 2606  3brtr3g 2636  axrep1 2684  axrep2 2685  axrep4 2687  axrep5 2688  class2set 2724  0inp0 2728  pwel 2749  exss 2759  opth1 2776  opth1gOLD 2788  opthwiener 2796  pwssun 2816  sotric 2851  difex2 2867  euuni 2871  reucl 2875  reuxfr2 2893  reuhyp 2895  iunpw 2904  efrn2lp 2919  epne3 2920  dfwe2 2925  wecmpep 2931  wereu 2935  ordtri3or 2969  ordtri1 2970  ordtri3 2973  ordeleqon 2980  sucexg 3039  suceloni 3052  ordnbtwn 3053  orddif 3065  orduniss 3066  ordtri2or 3067  ordunisuc 3079  suc11 3083  onelin 3093  onelun 3094  onuninsuc 3098  ordunisuc2 3105  dflim3 3108  limsssuc 3111  on0eqelt 3114  tfi 3116  find 3145  finds2 3148  tfindsg2 3153  ssrel 3237  elrel 3243  xpsspw 3247  relop 3265  dmxp 3321  resopab2 3382  relimasn 3409  ndmima 3418  funopg 3533  funun 3540  funcnvuni 3550  funin 3552  funcnvres2 3556  imadif 3560  fneu2 3579  fn0 3591  fnopabg 3601  fcoi2 3631  fcnvres 3633  f00 3642  foconst 3668  f1ococnv2 3693  f1ococnv1 3694  fvprc 3706  fv3 3718  tz6.12-2 3724  fvopabn 3771  elrnopabg 3785  exfo 3807  fopab2 3808  fsn 3819  fnressn 3822  tfrlem5 3900  tfrlem8 3903  tz7.48-2 3942  abianfp 3947  funoprabg 3995  curry1 4082  curry1f 4083  1stcof 4085  elrnoprabg 4108  oalimcl 4178  omlimcl 4193  brecop2 4291  ecopoprdm 4293  mapsn 4329  ixp0 4345  en2d 4381  dom2d 4385  fundmen 4409  unen 4414  pw2en 4426  sbthlem3 4429  sbthlem4 4430  sbthlem5 4431  sbthlem6 4432  sdomdomtr 4449  fodomr 4463  xpen 4468  mapenlem2 4470  mapdom2 4474  mapxpen 4475  xpmapenlem3 4478  xpmapenlem5 4480  mapunen 4482  pwen 4483  ssenen 4484  nneneq 4492  php 4493  isfinite1 4510  infn0 4512  ssfi 4515  unblem2 4518  isfinite2 4523  unfi 4528  unifi 4532  fiint 4534  abfii2 4536  pwfilem 4544  zfregcl 4567  elirrv 4570  inf3lem3 4587  inf3lem6 4590  infeq5 4593  noinfep 4612  zfregs 4619  r1val1 4630  rankr1 4646  rankuni 4670  rankval4 4674  rankc2 4678  rankelun 4679  rankelpr 4680  rankelop 4681  rankxplim 4684  rankxplim3 4686  rankxpsuc 4687  hta 4700  aceq3lem 4704  aceq5lem4 4710  aceq5 4712  ac6lem 4726  ac9s 4736  kmlem1 4737  kmlem4 4740  kmlem5 4741  kmlem7 4743  kmlem11 4747  zorn2lem4 4763  zorn2lem6 4765  zorn 4769  fodomb 4772  brdom3 4773  brdom5 4774  brdom4 4775  imadomg 4778  cardmin 4832  cardprc 4833  alephnbtwn 4840  cardaleph 4857  alephval3 4875  cflem 4877  cfval 4878  cfeq0 4886  cdavalt 4891  nd1 4910  nd2 4911  axpownd 4925  zfcndext 4937  zfcndrep 4938  distrpq 5039  prn0 5065  prnmax 5071  genpn0 5078  genpnnp 5080  prlem934 5111  ltaddpr 5112  prlem936 5127  reclem2pr 5129  suplem1pr 5133  suppsr 5194  supsrlem6 5202  ltresr 5230  supre 5232  negeu 5327  lttri4t 5487  ltnsym2t 5506  renfdisj 5512  xrltnsym2t 5524  xrrebndt 5541  receu 5670  rec11i 5733  eqneg 5760  nnind 5885  nn1suc 5887  nnleltp1t 5901  nominpos 5990  lble 5994  bndndx 6020  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  supxrre 6030  elnnz 6092  elnnz1 6102  uzwo3 6166  icounlem 6345  snunioolem 6347  uzwo 6387  uzwoOLD 6388  nnwof 6391  elfzp1 6442  fzneuzt 6450  expnnvalt 6504  discrlem3 6588  nn0opthlem2 6595  nn0opth 6596  sqrlem13 6615  sqr2irrlem3 6656  crulem 6666  crne0 6670  creui 6674  replimt 6692  abssubne0t 6820  cvg1 6858  cvg2 6859  cvg3 6860  faclbnd4lem4 6888  dffsum 6936  serzfsum 6942  fsump1s 6951  fsum1ps 6956  fsumshft 6969  fsumcmp 6978  bcxmas 7014  clm3 7017  climreu 7038  climrecl 7047  climge0 7049  climubi 7089  dfisum 7127  infcvglem1 7156  infcvglem3 7158  cvgratlem5 7189  fsum0diag4 7196  cncffvrn 7208  abscncflem 7209  mulc1cncf 7214  ivthlem3 7218  ivthlem5 7220  ivthlem6 7221  ivthlem7 7222  ivthlem4OLD 7228  ivthlem5OLD 7229  ivthlem6OLD 7230  ivthlem7OLD 7231  efseq0ex 7253  efclt 7254  efcvg 7256  efcvgfsum 7257  reeftlclt 7322  eflt 7347  efcnlem1 7359  efcn 7363  sinbndt 7407  cosbndt 7408  acdc5lem1 7433  acdcALT 7438  unbenlem 7447  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem10 7504  infxpidmlem11 7505  infxpidmlem12 7506  iunctb 7517  basgen2t 7581  subbas 7586  fctop 7592  cctop 7594  clsval 7619  uncld 7623  ntrval2 7628  cmclsopn 7635  cmntrcld 7636  elcls 7646  neif 7656  0nnei 7667  islp2 7688  clslp 7689  qdensere 7691  idcn 7705  ismsg 7739  metreslem 7762  blf 7784  cncfmet 7844  lmuni 7886  lmsslem 7887  lmfexlem1 7891  metcnp4 7904  xplmi 7907  xpcn 7910  oprcn 7911  bopcnlem1 7915  bopcnlem4 7918  bcthlem4 7936  bcthlem7 7939  bcthlem9 7941  bcthlem14 7946  bcthlem28 7960  bcthlem29 7961  bcthlem30 7962  bcthlem31 7963  bcthlem33 7965  grpideu 7987  grprn 7990  isgrp2i 8011  grpinvf 8014  grpdivf 8020  resgrprn 8030  resgrprnOLD 8031  grplactf1o 8034  vcex 8137  nvvcop 8151  nvvop 8166  nvex 8169  nvmf 8206  sqcn 8270  va1cnlem 8279  ipf 8300  ip1cnilem2 8308  ip1cnilem3 8309  nmlno0lem 8385  siilem1 8442  ipblnfi 8447  ubthlem3 8462  minveclem26 8501  pilem1 8590  pilem2 8591  sinperlem2 8606  sincosq2sgn 8622  sincosq4sgn 8624  efifolem2 8638  efif1lem5 8649  efif1lem7 8651  circcltOLD 8656  effoiOLD 8667  grothinf 8720  bcseq 8907  chcmh 9034  norm1ex 9043  shorth 9084  occllem4 9092  projlem24 9125  pjthlem11 9144  pjtheu2 9165  pjoc1 9179  spanvalt 9214  hsupval2t 9215  shlej1 9263  shs00 9288  chj00 9325  chabs2t 9355  h1de2 9391  cmbr4 9461  spansnm0 9512  nonbool 9513  5oalem5 9520  pjssm 9543  pjvect 9558  pjocvect 9559  hoaddclt 9601  homulclt 9602  eigpos 9679  dmadjopt 9737  brafnt 9787  kbopt 9793  nmlnop0ALT 9835  lnopeq0 9847  nmcopexlem4 9869  nmcfnexlem4 9898  cnlnadjlem2 9916  cnlnadjlem3 9917  cnlnadjlem4 9918  cnlnadjlem5 9919  cnlnssadj 9928  nmopco 9942  cnvbravalt 9956  kbass2t 9962  pjss1co 10002  pjss2co 10003  pjorthco 10008  pjscj 10009  pjssdif2 10013  pjssdif1 10014  pjclem4 10037  pjc 10038  pj3s 10045  pj3cor1 10047  strlem3a 10089  strlem6 10093  hstrlem3a 10097  hstrlem6 10101  mdbr3 10134  mdbr4 10135  ssmd2 10147  mdslj1 10154  mdslj2 10155  mdsl2b 10158  cvmd 10159  mdslmd1lem1 10160  mdslmd1lem2 10161  hatomistic 10197  chrelat2 10200  atssmat 10213  atoml2 10218  irredlem1 10225  irredlem2 10226  mdsymlem1 10238  mdsymlem2 10239  mdsymlem5 10242  dmdbr5at 10255  ghomfo 10296  ghomgsg 10300  ghomf1olem 10301  cayleylem2 10317  faimpex 10339  esnnei 10395  cnvhmpha 10412  hmphsyma 10415  hmphre 10417  hmeogrp 10425  homcard 10426  fillsb 10435  fipfil2 10439  efilcp 10445  filint2 10446  fgsb2 10449  efilcp2 10450  cnfilca 10451  dtt2 10462  trdom 10479  cnvtr 10482  homib 10568  hgrablkne0 10609

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