HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 sylib.1 . 2 |- (ph -> ps)
2 sylib.2 . . 3 |- (ps <-> ch)
32biimp 151 . 2 |- (ps -> ch)
41, 3syl 10 1 |- (ph -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  3imtr3 218  ord 232  exp3a 375  imdistand 445  bicomd 520  pm2.85 578  pm5.74d 584  mpbidi 588  negbid 610  pm4.71rd 638  pm5.32d 646  pm5.18 659  ecase2d 750  consensus 766  3mix3 816  ecase23d 920  excomim 1043  19.23ai 1062  19.23ad 1064  nexd 1100  sbf 1184  hbs1f 1187  sbied 1193  sbequi 1226  sbn 1229  a4sbe 1241  a4sbim 1242  a4sbbi 1243  sb6rf 1258  sb8 1259  sb9i 1261  eu2 1394  mooran1 1423  euor2 1435  2eu1 1447  eqcomd 1477  necon2bi 1609  necon2i 1610  necon4i 1622  necomd 1634  r19.21bi 1722  nrexdv 1727  elex 1815  ceqsalg 1821  cla4gf 1856  3sstr3g 2097  syl6ss 2103  sseq0 2300  un00 2302  npss0 2305  disjpss 2315  ssnelpss 2326  pssnel 2327  difsnid 2463  sneqr 2473  preqr1 2477  preq12b 2479  ssiun 2587  iununi 2611  3brtr3g 2641  axrep1 2689  axrep2 2690  axrep4 2692  axrep5 2693  class2set 2729  0inp0 2733  pwel 2754  exss 2764  opth1 2781  opthwiener 2802  pwssun 2822  sotric 2855  difex2 2872  euuni 2876  reucl 2880  reuxfr2 2898  reuhyp 2900  iunpw 2909  efrn2lp 2924  epne3 2925  dfwe2 2930  wecmpep 2936  wereu 2940  ordtri3or 2974  ordtri1 2975  ordtri3 2978  ordeleqon 2985  sucexg 3044  suceloni 3057  ordnbtwn 3058  orddif 3070  orduniss 3071  ordtri2or 3072  ordunisuc 3084  suc11 3088  onelin 3098  onelun 3099  onuninsuc 3103  ordunisuc2 3110  dflim3 3113  limsssuc 3116  on0eqelt 3119  tfi 3121  find 3150  finds2 3153  tfindsg2 3158  ssrel 3242  elrel 3248  xpsspw 3252  relop 3270  opelxpex2 3274  dmxp 3327  resopab2 3390  relimasn 3417  ndmima 3426  funopg 3539  funun 3546  funcnvuni 3556  funin 3558  funcnvres2 3562  imadif 3566  fneu2 3585  fn0 3597  fnopabg 3607  fcoi2 3637  fcnvres 3639  f00 3648  foconst 3674  f1ococnv2 3699  f1ococnv1 3700  fvprc 3712  fv3 3724  tz6.12-2 3730  fvopabn 3777  elrnopabg 3791  exfo 3813  fopab2 3814  fsn 3825  fnressn 3828  tfrlem5 3906  tfrlem8 3909  tz7.48-2 3948  abianfp 3953  funoprabg 4001  curry1 4088  curry1f 4089  1stcof 4091  elrnoprabg 4114  oalimcl 4184  omlimcl 4199  brecop2 4297  ecopoprdm 4299  mapsn 4335  ixp0 4351  en2d 4387  dom2d 4391  fundmen 4415  unen 4420  pw2en 4432  sbthlem3 4435  sbthlem4 4436  sbthlem5 4437  sbthlem6 4438  sdomdomtr 4455  fodomr 4469  xpen 4474  mapenlem2 4476  mapdom2 4480  mapxpen 4481  xpmapenlem3 4484  xpmapenlem5 4486  mapunen 4488  pwen 4489  ssenen 4490  nneneq 4498  php 4499  isfinite1 4516  infn0 4518  ssfi 4521  unblem2 4524  isfinite2 4529  unfi 4534  unifi 4538  fiint 4540  abfii2 4542  pwfilem 4550  zfregcl 4575  elirrv 4578  inf3lem3 4595  inf3lem6 4598  infeq5 4601  noinfep 4620  zfregs 4627  r1val1 4638  rankr1 4654  rankuni 4678  rankval4 4682  rankc2 4686  rankelun 4687  rankelpr 4688  rankelop 4689  rankxplim 4692  rankxplim3 4694  rankxpsuc 4695  hta 4708  aceq3lem 4712  aceq5lem4 4718  aceq5 4720  ac6lem 4734  ac9s 4744  kmlem1 4745  kmlem4 4748  kmlem5 4749  kmlem7 4751  kmlem11 4755  zorn2lem4 4771  zorn2lem6 4773  zorn 4777  fodomb 4780  brdom3 4781  brdom5 4782  brdom4 4783  imadomg 4786  cardmin 4840  cardprc 4841  alephnbtwn 4848  cardaleph 4865  alephval3 4883  cflem 4885  cfval 4886  cfeq0 4894  cdavalt 4899  nd1 4918  nd2 4919  axpownd 4933  zfcndext 4945  zfcndrep 4946  distrpq 5047  prn0 5073  prnmax 5079  genpn0 5086  genpnnp 5088  prlem934 5119  ltaddpr 5120  prlem936 5135  reclem2pr 5137  suplem1pr 5141  suppsr 5202  supsrlem6 5210  ltresr 5238  supre 5240  negeu 5335  lttri4t 5495  ltnsym2t 5514  renfdisj 5520  xrltnsym2t 5532  xrrebndt 5549  receu 5678  rec11i 5741  eqneg 5768  nnind 5893  nn1suc 5895  nnleltp1t 5909  nominpos 5998  lble 6002  bndndx 6028  xrsupsslem 6031  xrinfmsslem 6032  xrsupss 6033  xrinfmss 6034  supxrre 6038  elnnz 6100  elnnz1 6110  uzwo3 6174  icounlem 6353  snunioolem 6355  uzwo 6395  uzwoOLD 6396  nnwof 6399  elfzp1 6450  fzneuzt 6458  expnnvalt 6512  discrlem3 6596  nn0opthlem2 6603  nn0opth 6604  sqrlem13 6623  sqr2irrlem3 6664  crulem 6674  crne0 6678  creui 6682  replimt 6700  abssubne0t 6828  cvg1 6866  cvg2 6867  cvg3 6868  faclbnd4lem4 6896  dffsum 6944  serzfsum 6950  fsump1s 6959  fsum1ps 6964  fsumshft 6977  fsumcmp 6986  bcxmas 7022  clm3 7025  climreu 7046  climrecl 7055  climge0 7057  climubi 7097  dfisum 7135  infcvglem1 7164  infcvglem3 7166  cvgratlem5 7197  fsum0diag4 7204  cncffvrn 7216  abscncflem 7217  mulc1cncf 7222  ivthlem3 7226  ivthlem5 7228  ivthlem6 7229  ivthlem7 7230  ivthlem4OLD 7236  ivthlem5OLD 7237  ivthlem6OLD 7238  ivthlem7OLD 7239  efseq0ex 7261  efclt 7262  efcvg 7264  efcvgfsum 7265  reeftlclt 7330  eflt 7355  efcnlem1 7367  efcn 7371  sinbndt 7415  cosbndt 7416  acdc5lem1 7441  acdcALT 7446  unbenlem 7455  infxpidmlem7 7509  infxpidmlem8 7510  infxpidmlem10 7512  infxpidmlem11 7513  infxpidmlem12 7514  iunctb 7525  basgen2t 7589  subbas 7594  fctop 7600  cctop 7602  clsval 7627  uncld 7631  ntrval2 7636  cmclsopn 7643  cmntrcld 7644  elcls 7654  neif 7665  0nnei 7676  islp2 7697  clslp 7698  qdensere 7701  idcn 7716  ismsg 7750  metreslem 7774  blf 7796  cncfmet 7857  lmuni 7902  lmsslem 7903  lmfexlem1 7907  metcnp4 7920  xplmi 7923  xpcn 7926  oprcn 7927  bopcnlem1 7931  bopcnlem4 7934  bcthlem4 7952  bcthlem7 7955  bcthlem9 7957  bcthlem14 7962  bcthlem28 7976  bcthlem29 7977  bcthlem30 7978  bcthlem31 7979  bcthlem33 7981  grpideu 8003  grprn 8006  isgrp2i 8026  grpinvf 8029  grpdivf 8035  resgrprn 8045  resgrprnOLD 8046  grplactf1o 8049  vcex 8151  nvvcop 8165  nvvop 8180  nvex 8182  nvmf 8218  sqcn 8283  va1cnlem 8292  ipf 8313  ip1cnilem2 8321  ip1cnilem3 8322  nmlno0lem 8398  siilem1 8455  ipblnfi 8460  ubthlem3 8475  minveclem26 8514  pilem1 8609  pilem2 8610  sinperlem2 8625  sincosq2sgn 8641  sincosq4sgn 8643  efifolem2 8657  efif1lem5 8668  efif1lem7 8670  circcltOLD 8675  grothinf 8720  axhcompl 8807  bcseq 8925  chcmh 9052  norm1ex 9061  shorth 9107  occllem4 9115  projlem24 9148  pjthlem11 9167  pjtheu2 9188  pjoc1 9202  spanvalt 9237  hsupval2t 9238  shlej1 9286  shs00 9311  chj00 9348  chabs2t 9378  h1de2 9414  cmbr4 9484  spansnm0 9535  nonbool 9536  5oalem5 9543  pjssm 9566  pjvect 9581  pjocvect 9582  hoaddclt 9624  homulclt 9625  eigpos 9702  dmadjopt 9760  brafnt 9810  kbopt 9816  nmlnop0ALT 9858  lnopeq0 9870  nmcopexlem4 9892  nmcfnexlem4 9921  cnlnadjlem2 9939  cnlnadjlem3 9940  cnlnadjlem4 9941  cnlnadjlem5 9942  cnlnssadj 9951  nmopco 9966  cnvbravalt 9981  kbass2t 9988  pjss1co 10029  pjss2co 10030  pjorthco 10035  pjscj 10036  pjssdif2 10040  pjssdif1 10041  pjclem4 10065  pjc 10066  pj3s 10073  pj3cor1 10075  strlem3a 10117  strlem6 10121  hstrlem3a 10125  hstrlem6 10129  mdbr3 10162  mdbr4 10163  ssmd2 10176  mdslj1 10183  mdslj2 10184  mdsl2b 10187  cvmd 10188  mdslmd1lem1 10189  mdslmd1lem2 10190  hatomistic 10226  chrelat2 10229  atssmat 10242  atoml2 10247  irredlem1 10254  irredlem2 10255  mdsymlem1 10267  mdsymlem2 10268  mdsymlem5 10271  dmdbr5at 10284  ghomfo 10325  ghomgsg 10329  ghomf1olem 10330  cayleylem2 10344  faimpex 10375  esnnei 10431  cnvhmpha 10448  hmphsyma 10451  hmphre 10453  hmeogrp 10461  homcard 10462  fillsb 10471  fipfil2 10475  efilcp 10481  filint2 10482  fgsb2 10485  efilcp2 10486  cnfilca 10487  dtt2 10498  trdom 10515  cnvtr 10518  homib 10604  hgrablkne0 10645
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