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

Theorem syl5 30
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 28 . 2  |-  ( ph  ->  ( ch  ->  th )
)
43com12 29 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl56  32  syl2im  36  imim12i  55  pm2.86d  95  con2d  109  con3d  127  nsyli  135  syl5bi  209  syl5bir  210  syl5ib  211  adantld  454  adantrd  455  mpan9  456  pm4.79  567  pm2.36  817  pm4.72  847  ecased  911  ecase3ad  912  syl3an2  1218  alrimdh  1597  ax11w  1736  ax12dgen2  1741  ax5o  1765  spsd  1771  hbntOLD  1800  nfndOLD  1810  stdpc5OLD  1817  19.21hOLD  1862  cbv3hvOLD  1879  equs5e  1910  ax12olem1  2005  ax12olem1OLD  2011  ax12olem5OLD  2015  hbae  2040  hbaeOLD  2041  a16gOLD  2049  exdistrfOLD  2067  dvelimhOLD  2072  ax11a2  2080  sb4  2093  sbequi  2110  sbftOLD  2116  sbiedOLD  2151  ax11v  2172  ax11vALT  2173  ax5  2223  hbae-o  2230  dvelimf-o  2257  ax11indn  2272  ax11inda2  2276  ax11a2-o  2279  euimmo  2330  mopick  2343  spcimgft  3027  rr19.28v  3078  moeq3  3111  mob2  3114  euind  3121  reuind  3137  sbeqalb  3213  sbcimdv  3222  csbexg  3261  triun  4315  copsexg  4442  pwssun  4489  somo  4537  tz7.7  4607  ordunidif  4629  trsuc  4666  trsucss  4667  suc11  4685  reusv2lem2  4725  ralxfrd  4737  ralxfrALT  4742  onint  4775  limuni3  4832  tfi  4833  tfis  4834  tfinds  4839  limomss  4850  peano5  4868  relssres  5183  issref  5247  dmsnopg  5341  dfco2a  5370  imadif  5528  fvelima  5778  dffv2  5796  fvmptdf  5816  fvmptf  5821  fvmptnf  5822  foco2  5889  fconst5  5949  funfvima2  5974  funfvima3  5975  isores3  6055  oprabid  6105  ovmpt4g  6196  ovmpt2s  6197  ov2gf  6198  ovmpt2df  6205  suppss2  6300  suppssfv  6301  suppssov1  6302  fo2ndf  6453  frxp  6456  rntpos  6492  tposf2  6503  sorpsscmpl  6533  riotaxfrd  6581  riotasv3dOLD  6599  onfununi  6603  smofvon2  6618  smo11  6626  smoord  6627  tfrlem5  6641  tfrlem11  6649  tz7.44-2  6665  tz7.48lem  6698  tz7.48-1  6700  tz7.49  6702  tz7.49c  6703  omordi  6809  omord  6811  omass  6823  oneo  6824  omeulem1  6825  omopth2  6827  oewordri  6835  oeworde  6836  nnmordi  6874  nnmord  6875  omabs  6890  nnneo  6894  omsmo  6897  ectocld  6971  qsel  6983  eceqoveq  7009  mapsn  7055  f1oeng  7126  domunsncan  7208  sbthlem1  7217  2pwuninel  7262  mapen  7271  infensuc  7285  nneneq  7290  sucdom2  7303  pssnn  7327  dif1enOLD  7340  dif1en  7341  findcard2  7348  ac6sfi  7351  frfi  7352  unblem1  7359  unblem2  7360  unbnn2  7364  nnsdomg  7366  xpfi  7378  domunfican  7379  fiint  7383  fodomfi  7385  ixpfi2  7405  finsschain  7413  marypha1lem  7438  oiexg  7504  brwdom3  7550  sucprcreg  7567  inf3lem2  7584  inf3lem3  7585  noinfepOLD  7615  cantnfval2  7624  cantnflt  7627  cantnflem1  7645  cantnf  7649  cnfcom  7657  trcl  7664  epfrs  7667  r1sdom  7700  rankwflemb  7719  rankpwi  7749  rankelb  7750  carden2a  7853  cardsdomel  7861  carduni  7868  harval2  7884  pr2ne  7889  infpwfien  7943  cardaleph  7970  carduniima  7977  alephval3  7991  dfac5  8009  dfac12r  8026  dfac12k  8027  kmlem4  8033  kmlem11  8040  kmlem12  8041  cdainf  8072  infxp  8095  cfsuc  8137  cfcoflem  8152  coftr  8153  cfcof  8154  infpssr  8188  fin23lem30  8222  isf32lem1  8233  isf34lem6  8260  fin1a2lem13  8292  fin1a2s  8294  axcc2lem  8316  domtriomlem  8322  axdc4lem  8335  axcclem  8337  ac6num  8359  zorn2lem5  8380  zorn2lem6  8381  axdclem2  8400  alephval2  8447  alephreg  8457  pwcfsdom  8458  axpowndlem3  8474  axregndlem1  8477  axregnd  8479  axacndlem1  8482  axacndlem2  8483  axacndlem3  8484  axacndlem4  8485  axacnd  8487  gchi  8499  fpwwe2lem13  8517  canthp1  8529  gchpwdom  8549  wunfi  8596  tskwe2  8648  inar1  8650  gruen  8687  intgru  8689  indpi  8784  nqereu  8806  ltbtwnnq  8855  prnmadd  8874  genpcd  8883  prlem934  8910  ltexprlem1  8913  ltexprlem2  8914  ltexprlem7  8919  ltaprlem  8921  ltapr  8922  reclem4pr  8927  suplem2pr  8930  mulcmpblnr  8949  recexsrlem  8978  mulgt0sr  8980  recexsr  8982  supsrlem  8986  axpre-sup  9044  1re  9090  recex  9654  nnunb  10217  prime  10350  zeo  10355  fnn0ind  10369  zindd  10371  btwnz  10372  lbzbi  10564  xrub  10890  elfznelfzo  11192  facwordi  11580  fiinfnf1o  11634  hashclb  11641  hashdom  11653  hashf1lem2  11705  seqcoll  11712  limsupbnd2  12277  rlimdm  12345  o1of2  12406  rlimno1  12447  isercoll  12461  climcau  12464  caurcvg2  12471  caucvgb  12473  serf0  12474  zsum  12512  fsum2dlem  12554  fsum2d  12555  fsumabs  12580  fsumrlim  12590  fsumo1  12591  fsumiun  12600  incexclem  12616  odd2np1  12908  ndvdssub  12927  nprm  13093  maxprmfct  13113  rpexp  13120  pc2dvds  13252  pcfac  13268  unbenlem  13276  4sqlem12  13324  4sqlem17  13329  vdwlem6  13354  vdwlem13  13361  prmlem0  13428  xpscfv  13787  mreiincl  13821  sscfn1  14017  pospo  14430  cnvpsb  14645  dirref  14680  dirtr  14681  gaass  15074  elsymgbas  15097  cntz2ss  15131  odmulg  15192  odhash3  15210  sylow2alem1  15251  sylow2alem2  15252  pj1eu  15328  efgs1b  15368  efgsfo  15371  efgredlemc  15377  efgredeu  15384  frgpuptinv  15403  lt6abl  15504  ghmcyg  15505  ablfac1eulem  15630  pgpfac1lem5  15637  irredn1  15811  irredmul  15814  lspextmo  16132  lspsncv0  16218  mplcoe1  16528  mplcoe2  16530  cygth  16852  cnpco  17331  cnindis  17356  lmss  17362  lmcls  17366  lmcnp  17368  hausnei  17392  cmpsub  17463  tgcmp  17464  fiuncmp  17467  cmpfi  17471  1stcrest  17516  2ndcdisj  17519  1stccnp  17525  1stckgenlem  17585  txcls  17636  txcn  17658  txlm  17680  tx1stc  17682  txkgen  17684  xkococn  17692  hmphdis  17828  ptcmpfi  17845  isfild  17890  fgss2  17906  filcon  17915  trfil2  17919  ufileu  17951  filufint  17952  elfm2  17980  flftg  18028  cnpflf2  18032  fclssscls  18050  fclscf  18057  ufilcmp  18064  cnpfcf  18073  alexsubb  18077  alexsubALTlem4  18081  alexsubALT  18082  cnextcn  18098  divstgpopn  18149  tsmsxp  18184  isust  18233  xmettri2  18370  blin2  18459  setsmstopn  18508  met2ndc  18553  metcnp3  18570  tngtopn  18691  reconnlem2  18858  xrge0tsms  18865  fsumcn  18900  bndth  18983  iscmet3lem2  19245  iscmet3  19246  ivthlem1  19348  ivthlem2  19349  ivthlem3  19350  ovolfiniun  19397  volfiniun  19441  ioombl1lem4  19455  dyadmbl  19492  ismbf3d  19546  itg1addlem4  19591  mbfi1flimlem  19614  itg2seq  19634  itgfsum  19718  ellimc3  19766  dvmptfsum  19859  c1liplem1  19880  evlseu  19937  plypf1  20131  plydivex  20214  aannenlem1  20245  ulmval  20296  ulmcau  20311  ulmss  20313  ulmbdd  20314  ulmcn  20315  ulmdvlem3  20318  pserulm  20338  sineq0  20429  efopn  20549  cxpeq  20641  rlimcnp  20804  xrlimcnp  20807  perfectlem2  21014  lgsdir2lem2  21108  lgsne0  21117  2sqlem6  21153  2sqlem10  21158  dchrisumlem2  21184  crcts  21609  cycls  21610  usgrcyclnl1  21627  4cycl4dv  21654  isgrpo  21784  grpoidinvlem3  21794  gxcom  21857  gxinv  21858  gxid  21861  gxdi  21884  opidon  21910  exidu1  21914  rngoideu  21972  rngodi  21973  rngodir  21974  rngmgmbs4  22005  rngoridfz  22023  vcdi  22031  vcdir  22032  vcass  22033  nvs  22151  nvtri  22159  blocnilem  22305  chintcli  22833  hsupss  22843  shlej1  22862  elspansn4  23075  spansncvi  23154  hoaddsub  23319  lnopl  23417  lnfnl  23434  riesz4i  23566  pjnormssi  23671  pj3si  23710  stlei  23743  stcltr2i  23778  dmdmd  23803  dmdbr5  23811  mdslmd1lem2  23829  atssma  23881  atcvatlem  23888  chirredlem1  23893  atcvat4i  23900  mdsymlem2  23907  mdsymlem6  23911  sumdmdlem2  23922  dmdbr5ati  23925  cdjreui  23935  elimifd  24004  disjxpin  24028  suppss2f  24049  xrge0tsmsd  24223  lmxrge0  24337  ismeas  24553  conpcon  24922  cvmseu  24963  cvmliftlem15  24985  cvmlift2lem1  24989  cvmlift2lem12  25001  ghomf1olem  25105  dedekindle  25188  zprod  25263  fprod2dlem  25304  fprod2d  25305  dfpo2  25378  fundmpss  25390  dfon2lem3  25412  dfon2lem4  25413  dfon2lem6  25415  dfon2lem8  25417  dfon2lem9  25418  hbntg  25433  tfisg  25479  wfisg  25484  dftrpred3g  25511  trpredrec  25516  frinsg  25520  soseq  25529  wfr3g  25537  wfrlem4  25541  wfrlem5  25542  frr3g  25581  frrlem4  25585  frrlem5  25586  sltval2  25611  nodenselem5  25640  axlowdimlem16  25896  axcontlem2  25904  cgrdegen  25938  funtransport  25965  ifscgr  25978  cgrxfr  25989  brofs2  26011  brifs2  26012  idinside  26018  btwnconn1lem7  26027  btwnconn1lem11  26031  btwnconn1lem12  26032  btwnconn1lem14  26034  broutsideof2  26056  btwnoutside  26059  outsideoftr  26063  ontgval  26181  ordtop  26186  ordcmp  26197  onint1  26199  wl-bitr1  26220  voliunnfl  26250  volsupnfl  26251  itg2addnclem2  26257  itg2addnc  26259  itg2gt0cn  26260  ftc2nc  26289  finminlem  26321  ntruni  26330  comppfsc  26387  neibastop1  26388  filbcmb  26442  sdclem2  26446  seqpo  26451  nninfnub  26455  neificl  26459  prdstotbnd  26503  cnpwstotbnd  26506  heibor1lem  26518  heibor  26530  bfplem2  26532  grpokerinj  26560  divrngidl  26638  prnc  26677  prter2  26730  isnacs3  26764  pellexlem5  26896  pellex  26898  jm2.18  27059  jm2.15nn0  27074  jm2.16nn0  27075  setindtr  27095  dford3lem2  27098  ttac  27107  pmtrfrn  27377  psgnghm  27414  acsfn1p  27484  pm11.71  27573  ax10ext  27583  reuimrmo  27932  afvelima  28007  rlimdmafv  28017  ralxfrd2  28072  0mnnnnn0  28095  swrdccatin12lem3a  28208  el2wlkonot  28336  2wlkonot3v  28342  2spthonot3v  28343  2pthfrgra  28401  hbntal  28640  eel2221  28804  eel2122old  28828  bnj849  29296  bnj1110  29351  hbaewAUX7  29478  dvelimhvAUX7  29492  exdistrfNEW7  29505  ax11a2NEW7  29531  sbiedNEW7  29540  a16gNEW7  29546  sb4NEW7  29552  sbftNEW7  29556  ax11vNEW7  29595  hbaew0AUX7  29647  hbaew4AUX7  29648  ax7w18AUX7  29677  hbaeOLD7  29708  dvelimhOLD7  29713  l1cvpat  29852  atcvrj0  30225  pmaple  30558  paddasslem5  30621  pclfinN  30697  osumcllem11N  30763  pexmidlem8N  30774  dvheveccl  31910  dihord6apre  32054  lpolconN  32285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator