MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5ibcom Unicode version

Theorem syl5ibcom 212
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1  |-  ( ph  ->  ps )
syl5ib.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibcom  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3  |-  ( ph  ->  ps )
2 syl5ib.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2syl5ib 211 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 29 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  biimpcd  216  mob2  3074  rmob  3209  disjxun  4170  sotric  4489  sotrieq  4490  nordeq  4560  nsuceq0  4621  suctr  4624  dfwe2  4721  iss  5148  poirr2  5217  xp11  5263  tz6.12c  5709  fnbrfvb  5726  foeqcnvco  5986  f1eqcocnv  5987  tfrlem15  6612  tz7.44-2  6624  tz7.48-1  6659  tz7.49  6661  oawordexr  6758  oewordi  6793  oeeulem  6803  nna0r  6811  nnawordex  6839  nnaordex  6840  oaabs  6846  oaabs2  6847  ectocld  6930  ecoptocl  6953  mapsn  7014  eqeng  7100  difsnen  7149  fopwdom  7175  frfi  7311  elfiun  7393  ordiso  7441  ordtypelem7  7449  wemaplem2  7472  suc11reg  7530  inf3lem6  7544  noinfep  7570  cantnff  7585  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1  7601  cantnf  7605  r111  7657  rankc2  7753  tcrank  7764  cardnueq0  7807  fodomfi2  7897  alephinit  7932  dfac9  7972  dfac12k  7983  cdainf  8028  ackbij1  8074  ackbij2  8079  sornom  8113  fin23lem16  8171  fin23lem21  8175  isf32lem2  8190  fin1a2lem6  8241  itunitc  8257  zorn2lem4  8335  wunr1om  8550  tskr1om  8598  recmulnq  8797  ltexnq  8808  distrlem4pr  8859  1re  9046  0re  9047  0cnALT  9251  mulge0  9501  prodgt0  9811  peano2nn  9968  recnz  10301  zneo  10308  uzn0  10457  xlemul1a  10823  prunioo  10981  flidz  11173  modid2  11226  om2uzrani  11247  uzrdgfni  11253  seqid  11323  seqz  11326  facdiv  11533  facwordi  11535  hashdom  11608  sqrmo  12012  fsumf1o  12472  isumltss  12583  supcvg  12590  dvdsnegb  12822  odd2np1lem  12862  odd2np1  12863  bitsuz  12941  bezoutlem4  12996  gcddiv  13004  gcdeq  13007  dvdssqim  13008  dvdsprm  13054  coprm  13055  coprmdvds2  13058  prmdvdsexp  13069  rpmul  13078  prmdiv  13129  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pythagtriplem19  13162  pc2dvds  13207  pcadd  13213  prmpwdvds  13227  vdwlem11  13314  ramubcl  13341  0ram  13343  mreexexd  13828  posasymb  14364  pleval2  14377  pltval3  14379  plttr  14382  pospo  14385  letsr  14627  ismgmid  14665  imasmnd2  14687  isgrpid2  14796  isgrpinv  14810  imasgrp2  14888  orbsta  15045  odmulg  15147  odmulgeq  15148  gexdvdsi  15172  gexnnod  15177  pgpssslw  15203  sylow2alem1  15206  fislw  15214  lsmss1b  15254  lsmss2b  15256  efgrelexlemb  15337  torsubg  15424  ablfacrplem  15578  pgpfac1lem2  15588  pgpfac1lem3  15590  imasrng  15680  dvdsrcl2  15710  dvdsrtr  15712  dvdsrmul1  15713  irredn0  15763  lspsneq0  16043  lmhmima  16078  lspsolv  16170  opsrtoslem2  16500  xrsdsreclblem  16699  dvdsrz  16722  prmirredlem  16728  znunit  16799  pjdm2  16893  obselocv  16910  baspartn  16974  bastop  17001  iscld3  17083  isopn3  17085  iscldtop  17114  ordtrest2lem  17221  2ndcredom  17466  2ndc1stc  17467  2ndcrest  17470  2ndcdisj  17472  2ndcsep  17475  kgenidm  17532  dfac14  17603  tx2ndc  17636  kqreglem1  17726  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  flimtopon  17955  fclstopon  17997  xrsmopn  18796  icccmplem2  18807  reconnlem1  18810  iccpnfcnv  18922  cphsqrcl2  19102  ivthlem3  19303  ivthicc  19308  ovolctb  19339  ioombl  19412  itgabs  19679  itgsplitioo  19682  dvlip  19830  c1liplem1  19833  c1lip1  19834  dvgt0lem1  19839  dvivthlem2  19846  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvcvx  19857  itgsubstlem  19885  mpfind  19918  mpfpf1  19924  pf1mpf  19925  mdegnn0cl  19947  ig1peu  20047  elply2  20068  plypf1  20084  dgreq0  20136  aannenlem3  20200  abelthlem2  20301  lognegb  20437  eflogeq  20449  efopn  20502  cxpge0  20527  cxplea  20540  cxple2  20541  cxpcn3lem  20584  cxpaddlelem  20588  cxpaddle  20589  cxpeq  20594  asinsinb  20690  acoscosb  20691  atantanb  20717  leibpilem1  20733  wilthlem2  20805  sqf11  20875  sqff1o  20918  ppiublem1  20939  lgsdir  21067  lgsne0  21070  lgsquadlem3  21093  2sqblem  21114  dchrisum0flblem1  21155  ostth3  21285  ostth  21286  umgraf  21306  usgrcyclnl1  21580  nvnencycllem  21583  eupath2lem2  21653  eupath2lem3  21654  isgrp2d  21776  rngosn3  21967  htthlem  22373  pjpreeq  22853  h1dn0  23007  spansneleqi  23024  rnbra  23563  dfpjop  23638  elpjrn  23646  stm1i  23699  mdbr2  23752  mdsl2i  23778  sumdmdlem  23874  dmdbr6ati  23879  xrge0iifcnv  24272  erdszelem8  24837  cvmlift3lem4  24962  cvmlift3lem5  24963  ghomgrpilem2  25050  dvdspw  25317  dfon2lem9  25361  poseq  25467  nodenselem3  25551  nodenselem5  25553  nodenselem8  25556  nofulllem5  25574  colinearalg  25753  axcontlem5  25811  axcontlem9  25815  btwnconn1lem11  25935  broutsideof2  25960  itgabsnc  26173  opnbnd  26218  tailfb  26296  sdclem2  26336  subspopn  26348  equivtotbnd  26377  igenval2  26566  isfldidl  26568  ismrc  26645  pellexlem1  26782  aomclem4  27022  dfac21  27032  lsmfgcl  27040  lmhmfgima  27050  dfacbasgrp  27141  lindfrn  27159  hbtlem6  27201  pmtrfrn  27268  fiuneneq  27381  xrltneNEW  27524  stoweidlem27  27643  stoweidlem29  27645  usg2wlkonot  28080  usg2wotspth  28081  lshpinN  29472  lsatcv0eq  29530  lsatcv1  29531  cvrnbtwn3  29759  cvrnbtwn4  29762  cvrcmp  29766  atnlt  29796  cvlexchb1  29813  2llnne2N  29890  atcvr0eq  29908  lnnat  29909  cvrat4  29925  ps-1  29959  3at  29972  llncmp  30004  llnnlt  30005  llncvrlpln2  30039  llncvrlpln  30040  lplncmp  30044  lplnnlt  30047  lplncvrlvol2  30097  lplncvrlvol  30098  lvolcmp  30099  lvolnltN  30100  dalempnes  30133  dalemqnet  30134  dalem-cly  30153  dalem44  30198  lncmp  30265  cdlemblem  30275  llnexch2N  30352  osumcllem4N  30441  pexmidlem1N  30452  lhp2atnle  30515  cdleme11dN  30744  cdleme20k  30801  cdleme21at  30810  cdleme21ct  30811  cdleme32e  30927  cdleme35f  30936  tendoex  31457  dochexmidlem1  31943  lcfrlem9  32033  mapd1o  32131  mapdindp3  32205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator