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

Theorem syl5 31
Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)
Hypotheses
Ref Expression
syl5.1  |-  ( ph  ->  ps )
syl5.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3  |-  ( ph  ->  ps )
2 syl5.2 . . 3  |-  ( ch 
->  ( ps  ->  th )
)
31, 2syl5com 29 . 2  |-  ( ph  ->  ( ch  ->  th )
)
43com12 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl56  33  syl2im  37  imim12i  56  pm2.86d  96  con2d  110  con3d  128  nsyli  136  syl5bi  210  syl5bir  211  syl5ib  212  adantld  455  adantrd  456  mpan9  457  pm4.79  568  pm2.36  818  pm4.72  848  ecased  912  ecase3ad  913  syl3an2  1219  alrimdh  1598  ax11w  1737  ax12dgen2  1742  ax5o  1766  spsd  1772  hbntOLD  1801  nfndOLD  1811  stdpc5OLD  1818  19.21hOLD  1863  cbv3hvOLD  1880  equs5e  1911  ax12olem1  2006  ax12olem1OLD  2012  ax12olem5OLD  2016  hbae  2041  hbaeOLD  2042  a16gOLD  2050  exdistrfOLD  2068  dvelimhOLD  2073  ax11a2  2081  sb4  2094  sbequi  2111  sbftOLD  2117  sbiedOLD  2152  ax11v  2173  ax11vALT  2174  ax5  2224  hbae-o  2231  dvelimf-o  2258  ax11indn  2273  ax11inda2  2277  ax11a2-o  2280  euimmo  2331  mopick  2344  spcimgft  3028  rr19.28v  3079  moeq3  3112  mob2  3115  euind  3122  reuind  3138  sbeqalb  3214  sbcimdv  3223  csbexg  3262  triun  4316  copsexg  4443  pwssun  4490  somo  4538  tz7.7  4608  ordunidif  4630  trsuc  4667  trsucss  4668  suc11  4686  reusv2lem2  4726  ralxfrd  4738  ralxfrALT  4743  onint  4776  limuni3  4833  tfi  4834  tfis  4835  tfinds  4840  limomss  4851  peano5  4869  relssres  5184  issref  5248  dmsnopg  5342  dfco2a  5371  imadif  5529  fvelima  5779  dffv2  5797  fvmptdf  5817  fvmptf  5822  fvmptnf  5823  foco2  5890  fconst5  5950  funfvima2  5975  funfvima3  5976  isores3  6056  oprabid  6106  ovmpt4g  6197  ovmpt2s  6198  ov2gf  6199  ovmpt2df  6206  suppss2  6301  suppssfv  6302  suppssov1  6303  fo2ndf  6454  frxp  6457  rntpos  6493  tposf2  6504  sorpsscmpl  6534  riotaxfrd  6582  riotasv3dOLD  6600  onfununi  6604  smofvon2  6619  smo11  6627  smoord  6628  tfrlem5  6642  tfrlem11  6650  tz7.44-2  6666  tz7.48lem  6699  tz7.48-1  6701  tz7.49  6703  tz7.49c  6704  omordi  6810  omord  6812  omass  6824  oneo  6825  omeulem1  6826  omopth2  6828  oewordri  6836  oeworde  6837  nnmordi  6875  nnmord  6876  omabs  6891  nnneo  6895  omsmo  6898  ectocld  6972  qsel  6984  eceqoveq  7010  mapsn  7056  f1oeng  7127  domunsncan  7209  sbthlem1  7218  2pwuninel  7263  mapen  7272  infensuc  7286  nneneq  7291  sucdom2  7304  pssnn  7328  dif1enOLD  7341  dif1en  7342  findcard2  7349  ac6sfi  7352  frfi  7353  unblem1  7360  unblem2  7361  unbnn2  7365  nnsdomg  7367  xpfi  7379  domunfican  7380  fiint  7384  fodomfi  7386  ixpfi2  7406  finsschain  7414  marypha1lem  7439  oiexg  7505  brwdom3  7551  sucprcreg  7568  inf3lem2  7585  inf3lem3  7586  noinfepOLD  7616  cantnfval2  7625  cantnflt  7628  cantnflem1  7646  cantnf  7650  cnfcom  7658  trcl  7665  epfrs  7668  r1sdom  7701  rankwflemb  7720  rankpwi  7750  rankelb  7751  carden2a  7854  cardsdomel  7862  carduni  7869  harval2  7885  pr2ne  7890  infpwfien  7944  cardaleph  7971  carduniima  7978  alephval3  7992  dfac5  8010  dfac12r  8027  dfac12k  8028  kmlem4  8034  kmlem11  8041  kmlem12  8042  cdainf  8073  infxp  8096  cfsuc  8138  cfcoflem  8153  coftr  8154  cfcof  8155  infpssr  8189  fin23lem30  8223  isf32lem1  8234  isf34lem6  8261  fin1a2lem13  8293  fin1a2s  8295  axcc2lem  8317  domtriomlem  8323  axdc4lem  8336  axcclem  8338  ac6num  8360  zorn2lem5  8381  zorn2lem6  8382  axdclem2  8401  alephval2  8448  alephreg  8458  pwcfsdom  8459  axpowndlem3  8475  axregndlem1  8478  axregnd  8480  axacndlem1  8483  axacndlem2  8484  axacndlem3  8485  axacndlem4  8486  axacnd  8488  gchi  8500  fpwwe2lem13  8518  canthp1  8530  gchpwdom  8550  wunfi  8597  tskwe2  8649  inar1  8651  gruen  8688  intgru  8690  indpi  8785  nqereu  8807  ltbtwnnq  8856  prnmadd  8875  genpcd  8884  prlem934  8911  ltexprlem1  8914  ltexprlem2  8915  ltexprlem7  8920  ltaprlem  8922  ltapr  8923  reclem4pr  8928  suplem2pr  8931  mulcmpblnr  8950  recexsrlem  8979  mulgt0sr  8981  recexsr  8983  supsrlem  8987  axpre-sup  9045  1re  9091  recex  9655  nnunb  10218  prime  10351  zeo  10356  fnn0ind  10370  zindd  10372  btwnz  10373  lbzbi  10565  xrub  10891  elfznelfzo  11193  facwordi  11581  fiinfnf1o  11635  hashclb  11642  hashdom  11654  hashf1lem2  11706  seqcoll  11713  limsupbnd2  12278  rlimdm  12346  o1of2  12407  rlimno1  12448  isercoll  12462  climcau  12465  caurcvg2  12472  caucvgb  12474  serf0  12475  zsum  12513  fsum2dlem  12555  fsum2d  12556  fsumabs  12581  fsumrlim  12591  fsumo1  12592  fsumiun  12601  incexclem  12617  odd2np1  12909  ndvdssub  12928  nprm  13094  maxprmfct  13114  rpexp  13121  pc2dvds  13253  pcfac  13269  unbenlem  13277  4sqlem12  13325  4sqlem17  13330  vdwlem6  13355  vdwlem13  13362  prmlem0  13429  xpscfv  13788  mreiincl  13822  sscfn1  14018  pospo  14431  cnvpsb  14646  dirref  14681  dirtr  14682  gaass  15075  elsymgbas  15098  cntz2ss  15132  odmulg  15193  odhash3  15211  sylow2alem1  15252  sylow2alem2  15253  pj1eu  15329  efgs1b  15369  efgsfo  15372  efgredlemc  15378  efgredeu  15385  frgpuptinv  15404  lt6abl  15505  ghmcyg  15506  ablfac1eulem  15631  pgpfac1lem5  15638  irredn1  15812  irredmul  15815  lspextmo  16133  lspsncv0  16219  mplcoe1  16529  mplcoe2  16531  cygth  16853  cnpco  17332  cnindis  17357  lmss  17363  lmcls  17367  lmcnp  17369  hausnei  17393  cmpsub  17464  tgcmp  17465  fiuncmp  17468  cmpfi  17472  1stcrest  17517  2ndcdisj  17520  1stccnp  17526  1stckgenlem  17586  txcls  17637  txcn  17659  txlm  17681  tx1stc  17683  txkgen  17685  xkococn  17693  hmphdis  17829  ptcmpfi  17846  isfild  17891  fgss2  17907  filcon  17916  trfil2  17920  ufileu  17952  filufint  17953  elfm2  17981  flftg  18029  cnpflf2  18033  fclssscls  18051  fclscf  18058  ufilcmp  18065  cnpfcf  18074  alexsubb  18078  alexsubALTlem4  18082  alexsubALT  18083  cnextcn  18099  divstgpopn  18150  tsmsxp  18185  isust  18234  xmettri2  18371  blin2  18460  setsmstopn  18509  met2ndc  18554  metcnp3  18571  tngtopn  18692  reconnlem2  18859  xrge0tsms  18866  fsumcn  18901  bndth  18984  iscmet3lem2  19246  iscmet3  19247  ivthlem1  19349  ivthlem2  19350  ivthlem3  19351  ovolfiniun  19398  volfiniun  19442  ioombl1lem4  19456  dyadmbl  19493  ismbf3d  19547  itg1addlem4  19592  mbfi1flimlem  19615  itg2seq  19635  itgfsum  19719  ellimc3  19767  dvmptfsum  19860  c1liplem1  19881  evlseu  19938  plypf1  20132  plydivex  20215  aannenlem1  20246  ulmval  20297  ulmcau  20312  ulmss  20314  ulmbdd  20315  ulmcn  20316  ulmdvlem3  20319  pserulm  20339  sineq0  20430  efopn  20550  cxpeq  20642  rlimcnp  20805  xrlimcnp  20808  perfectlem2  21015  lgsdir2lem2  21109  lgsne0  21118  2sqlem6  21154  2sqlem10  21159  dchrisumlem2  21185  crcts  21610  cycls  21611  usgrcyclnl1  21628  4cycl4dv  21655  isgrpo  21785  grpoidinvlem3  21795  gxcom  21858  gxinv  21859  gxid  21862  gxdi  21885  opidon  21911  exidu1  21915  rngoideu  21973  rngodi  21974  rngodir  21975  rngmgmbs4  22006  rngoridfz  22024  vcdi  22032  vcdir  22033  vcass  22034  nvs  22152  nvtri  22160  blocnilem  22306  chintcli  22834  hsupss  22844  shlej1  22863  elspansn4  23076  spansncvi  23155  hoaddsub  23320  lnopl  23418  lnfnl  23435  riesz4i  23567  pjnormssi  23672  pj3si  23711  stlei  23744  stcltr2i  23779  dmdmd  23804  dmdbr5  23812  mdslmd1lem2  23830  atssma  23882  atcvatlem  23889  chirredlem1  23894  atcvat4i  23901  mdsymlem2  23908  mdsymlem6  23912  sumdmdlem2  23923  dmdbr5ati  23926  cdjreui  23936  elimifd  24005  disjxpin  24029  suppss2f  24050  xrge0tsmsd  24224  lmxrge0  24338  ismeas  24554  conpcon  24923  cvmseu  24964  cvmliftlem15  24986  cvmlift2lem1  24990  cvmlift2lem12  25002  ghomf1olem  25106  dedekindle  25189  zprod  25264  fprod2dlem  25305  fprod2d  25306  dfpo2  25379  fundmpss  25391  dfon2lem3  25413  dfon2lem4  25414  dfon2lem6  25416  dfon2lem8  25418  dfon2lem9  25419  hbntg  25434  tfisg  25480  wfisg  25485  dftrpred3g  25512  trpredrec  25517  frinsg  25521  soseq  25530  wfr3g  25538  wfrlem4  25542  wfrlem5  25543  frr3g  25582  frrlem4  25586  frrlem5  25587  sltval2  25612  nodenselem5  25641  axlowdimlem16  25897  axcontlem2  25905  cgrdegen  25939  funtransport  25966  ifscgr  25979  cgrxfr  25990  brofs2  26012  brifs2  26013  idinside  26019  btwnconn1lem7  26028  btwnconn1lem11  26032  btwnconn1lem12  26033  btwnconn1lem14  26035  broutsideof2  26057  btwnoutside  26060  outsideoftr  26064  ontgval  26182  ordtop  26187  ordcmp  26198  onint1  26200  wl-bitr1  26221  voliunnfl  26251  volsupnfl  26252  itg2addnclem2  26258  itg2addnc  26260  itg2gt0cn  26261  ftc2nc  26290  finminlem  26322  ntruni  26331  comppfsc  26388  neibastop1  26389  filbcmb  26443  sdclem2  26447  seqpo  26452  nninfnub  26456  neificl  26460  prdstotbnd  26504  cnpwstotbnd  26507  heibor1lem  26519  heibor  26531  bfplem2  26533  grpokerinj  26561  divrngidl  26639  prnc  26678  prter2  26731  isnacs3  26765  pellexlem5  26897  pellex  26899  jm2.18  27060  jm2.15nn0  27075  jm2.16nn0  27076  setindtr  27096  dford3lem2  27099  ttac  27108  pmtrfrn  27378  psgnghm  27415  acsfn1p  27485  pm11.71  27574  ax10ext  27584  reuimrmo  27933  afvelima  28008  rlimdmafv  28018  ralxfrd2  28073  0mnnnnn0  28096  swrdccatin12lem3a  28209  el2wlkonot  28337  2wlkonot3v  28343  2spthonot3v  28344  2pthfrgra  28402  hbntal  28641  eel2221  28805  eel2122old  28829  bnj849  29297  bnj1110  29352  hbaewAUX7  29479  dvelimhvAUX7  29493  exdistrfNEW7  29506  ax11a2NEW7  29532  sbiedNEW7  29541  a16gNEW7  29547  sb4NEW7  29553  sbftNEW7  29557  ax11vNEW7  29596  hbaew0AUX7  29648  hbaew4AUX7  29649  ax7w18AUX7  29678  hbaeOLD7  29709  dvelimhOLD7  29714  l1cvpat  29853  atcvrj0  30226  pmaple  30559  paddasslem5  30622  pclfinN  30698  osumcllem11N  30764  pexmidlem8N  30775  dvheveccl  31911  dihord6apre  32055  lpolconN  32286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator