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

Theorem syl5 28
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 26 . 2  |-  ( ph  ->  ( ch  ->  th )
)
43com12 27 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl56  30  syl2im  34  imim12i  53  pm2.86d  93  con2d  107  con3d  125  nsyli  133  syl5bi  208  syl5bir  209  syl5ib  210  adantld  453  adantrd  454  mpan9  455  pm4.79  566  pm2.36  816  pm4.72  846  ecased  910  ecase3ad  911  syl3an2  1216  alrimdh  1574  ax11w  1695  ax12dgen2  1700  ax5o  1717  hbnt  1724  19.21h  1731  cbv3hv  1737  spsd  1740  nfnd  1760  stdpc5  1793  ax12olem5  1872  a16g  1885  hbae  1893  dvelimh  1904  exdistrf  1911  ax11a2  1933  sbft  1965  sbied  1976  sb4  1993  ax11v  2036  ax5  2085  hbae-o  2092  dvelimf-o  2119  ax11indn  2134  ax11inda2  2138  ax11a2-o  2141  euimmo  2192  mopick  2205  spcimgft  2859  rr19.28v  2910  moeq3  2942  mob2  2945  euind  2952  reuind  2968  sbeqalb  3043  sbcimdv  3052  csbexg  3091  triun  4126  copsexg  4252  pwssun  4299  somo  4348  tz7.7  4418  ordunidif  4440  trsuc  4476  trsuc2OLD  4477  trsucss  4478  suc11  4496  reusv2lem2  4536  ralxfrd  4548  ralxfrALT  4553  onint  4586  limuni3  4643  tfi  4644  tfis  4645  tfinds  4650  limomss  4661  peano5  4679  relssres  4992  issref  5056  dmsnopg  5144  dfco2a  5173  imadif  5327  fvelima  5574  dffv2  5592  fvmptdf  5611  fvmptf  5616  fvmptnf  5617  foco2  5680  fconst5  5731  funfvima2  5754  funfvima3  5755  isores3  5832  oprabid  5882  ovmpt4g  5970  ovmpt2s  5971  ov2gf  5972  ovmpt2df  5979  suppss2  6073  suppssfv  6074  suppssov1  6075  frxp  6225  rntpos  6247  tposf2  6258  sorpsscmpl  6288  riotaxfrd  6336  riotasv3dOLD  6354  onfununi  6358  smofvon2  6373  smo11  6381  smoord  6382  tfrlem5  6396  tfrlem11  6404  tz7.44-2  6420  tz7.48lem  6453  tz7.48-1  6455  tz7.49  6457  tz7.49c  6458  omordi  6564  omord  6566  omass  6578  oneo  6579  omeulem1  6580  omopth2  6582  oewordri  6590  oeworde  6591  nnmordi  6629  nnmord  6630  omabs  6645  nnneo  6649  omsmo  6652  ectocld  6726  qsel  6738  eceqoveq  6763  mapsn  6809  f1oeng  6880  domunsncan  6962  sbthlem1  6971  2pwuninel  7016  mapen  7025  infensuc  7039  nneneq  7044  sucdom2  7057  pssnn  7081  dif1enOLD  7090  dif1en  7091  findcard2  7098  ac6sfi  7101  frfi  7102  unblem1  7109  unblem2  7110  unbnn2  7114  nnsdomg  7116  xpfi  7128  domunfican  7129  fiint  7133  fodomfi  7135  ixpfi2  7154  finsschain  7162  marypha1lem  7186  oiexg  7250  brwdom3  7296  sucprcreg  7313  inf3lem2  7330  inf3lem3  7331  noinfepOLD  7361  cantnfval2  7370  cantnflt  7373  cantnflem1  7391  cantnf  7395  cnfcom  7403  trcl  7410  epfrs  7413  r1sdom  7446  rankwflemb  7465  rankpwi  7495  rankelb  7496  carden2a  7599  cardsdomel  7607  carduni  7614  harval2  7630  pr2ne  7635  infpwfien  7689  cardaleph  7716  carduniima  7723  alephval3  7737  dfac5  7755  dfac12r  7772  dfac12k  7773  kmlem4  7779  kmlem11  7786  kmlem12  7787  cdainf  7818  infxp  7841  cfsuc  7883  cfcoflem  7898  coftr  7899  cfcof  7900  infpssr  7934  fin23lem30  7968  isf32lem1  7979  isf34lem6  8006  fin1a2lem13  8038  fin1a2s  8040  axcc2lem  8062  domtriomlem  8068  axdc4lem  8081  axcclem  8083  ac6num  8106  zorn2lem5  8127  zorn2lem6  8128  axdclem2  8147  alephval2  8194  alephreg  8204  pwcfsdom  8205  axpowndlem3  8221  axregndlem1  8224  axregnd  8226  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacnd  8234  gchi  8246  fpwwe2lem13  8264  canthp1  8276  gchpwdom  8296  wunfi  8343  tskwe2  8395  inar1  8397  gruen  8434  intgru  8436  indpi  8531  nqereu  8553  ltbtwnnq  8602  prnmadd  8621  genpcd  8630  prlem934  8657  ltexprlem1  8660  ltexprlem2  8661  ltexprlem7  8666  ltaprlem  8668  ltapr  8669  reclem4pr  8674  suplem2pr  8677  mulcmpblnr  8696  recexsrlem  8725  mulgt0sr  8727  recexsr  8729  supsrlem  8733  axpre-sup  8791  1re  8837  recex  9400  nnunb  9961  prime  10092  zeo  10097  fnn0ind  10111  zindd  10113  btwnz  10114  lbzbi  10306  xrub  10630  facwordi  11302  hashclb  11352  hashdom  11361  hashf1lem2  11394  seqcoll  11401  limsupbnd2  11957  rlimdm  12025  o1of2  12086  rlimno1  12127  isercoll  12141  climcau  12144  caurcvg2  12150  caucvgb  12152  serf0  12153  zsum  12191  fsum2dlem  12233  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  incexclem  12295  odd2np1  12587  ndvdssub  12606  nprm  12772  maxprmfct  12792  rpexp  12799  pc2dvds  12931  pcfac  12947  unbenlem  12955  4sqlem12  13003  4sqlem17  13008  vdwlem6  13033  vdwlem13  13040  prmlem0  13107  xpscfv  13464  mreiincl  13498  catpropd  13612  sscfn1  13694  pospo  14107  cnvpsb  14322  dirref  14357  dirtr  14358  gaass  14751  elsymgbas  14774  cntz2ss  14808  odmulg  14869  odhash3  14887  sylow2alem1  14928  sylow2alem2  14929  pj1eu  15005  efgs1b  15045  efgsfo  15048  efgredlemc  15054  efgredeu  15061  frgpuptinv  15080  lt6abl  15181  ghmcyg  15182  ablfac1eulem  15307  pgpfac1lem5  15314  irredn1  15488  irredmul  15491  lspextmo  15813  lspsncv0  15899  mplcoe1  16209  mplcoe2  16211  cygth  16525  cnpco  16996  cnindis  17020  lmss  17026  lmcls  17030  lmcnp  17032  hausnei  17056  cmpsub  17127  tgcmp  17128  fiuncmp  17131  cmpfi  17135  1stcrest  17179  2ndcdisj  17182  1stccnp  17188  1stckgenlem  17248  txcls  17299  txcn  17320  txlm  17342  tx1stc  17344  txkgen  17346  xkococn  17354  hmphdis  17487  ptcmpfi  17504  isfild  17553  fgss2  17569  filcon  17578  trfil2  17582  ufileu  17614  filufint  17615  elfm2  17643  flftg  17691  cnpflf2  17695  fclssscls  17713  fclscf  17720  ufilcmp  17727  cnpfcf  17736  alexsubb  17740  alexsubALTlem4  17744  alexsubALT  17745  divstgpopn  17802  tsmsxp  17837  xmettri2  17905  blin2  17975  setsmstopn  18024  met2ndc  18069  metcnp3  18086  tngtopn  18166  reconnlem2  18332  xrge0tsms  18339  fsumcn  18374  bndth  18456  iscmet3lem2  18718  iscmet3  18719  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ovolfiniun  18860  volfiniun  18904  ioombl1lem4  18918  dyadmbl  18955  ismbf3d  19009  itg1addlem4  19054  mbfi1flimlem  19077  itg2seq  19097  itgfsum  19181  ellimc3  19229  dvmptfsum  19322  c1liplem1  19343  evlseu  19400  plypf1  19594  plydivex  19677  aannenlem1  19708  ulmval  19759  ulmcau  19772  ulmss  19774  ulmbdd  19775  ulmcn  19776  ulmdvlem3  19779  pserulm  19798  sineq0  19889  efopn  20005  cxpeq  20097  rlimcnp  20260  xrlimcnp  20263  perfectlem2  20469  lgsdir2lem2  20563  lgsne0  20572  2sqlem6  20608  2sqlem10  20613  dchrisumlem2  20639  isgrpo  20863  grpoidinvlem3  20873  gxcom  20936  gxinv  20937  gxid  20940  gxdi  20963  opidon  20989  exidu1  20993  rngoideu  21051  rngodi  21052  rngodir  21053  rngmgmbs4  21084  vcdi  21108  vcdir  21109  vcass  21110  nvs  21228  nvtri  21236  blocnilem  21382  chintcli  21910  hsupss  21920  shlej1  21939  elspansn4  22152  spansncvi  22231  hoaddsub  22396  lnopl  22494  lnfnl  22511  riesz4i  22643  pjnormssi  22748  pj3si  22787  stlei  22820  stcltr2i  22855  dmdmd  22880  dmdbr5  22888  mdslmd1lem2  22906  atssma  22958  atcvatlem  22965  chirredlem1  22970  atcvat4i  22977  mdsymlem2  22984  mdsymlem6  22988  sumdmdlem2  22999  dmdbr5ati  23002  cdjreui  23012  elimifd  23151  suppss2f  23201  unitdivcld  23285  lmxrge0  23375  xrge0tsmsd  23382  ismeas  23530  conpcon  23766  cvmseu  23807  cvmliftlem15  23829  cvmlift2lem1  23833  cvmlift2lem12  23845  ghomf1olem  24001  dedekindle  24083  dfpo2  24112  fundmpss  24122  dfon2lem3  24141  dfon2lem4  24142  dfon2lem6  24144  dfon2lem8  24146  dfon2lem9  24147  hbntg  24162  tfisg  24204  wfisg  24209  dftrpred3g  24236  trpredrec  24241  frinsg  24245  soseq  24254  wfr3g  24255  wfrlem4  24259  wfrlem5  24260  frr3g  24280  frrlem4  24284  frrlem5  24285  sltval2  24310  nodenselem5  24339  axlowdimlem16  24585  axcontlem2  24593  cgrdegen  24627  funtransport  24654  ifscgr  24667  cgrxfr  24678  brofs2  24700  brifs2  24701  idinside  24707  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem14  24723  broutsideof2  24745  btwnoutside  24748  outsideoftr  24752  ontgval  24870  ordtop  24875  ordcmp  24886  onint1  24888  wl-bitr1  24910  untind  25018  prl2  25169  domrancur1c  25202  valcurfn1  25204  rngoridfz  25437  intopcoaconlem3b  25538  hdrmp  25706  cmpassoh  25801  cmpmon  25815  idmon  25817  iepiclem  25823  propsrc  25868  finminlem  26231  ntruni  26245  comppfsc  26307  neibastop1  26308  filbcmb  26432  sdclem2  26452  seqpo  26457  nninfnub  26461  neificl  26467  prdstotbnd  26518  cnpwstotbnd  26521  heibor1lem  26533  heibor  26545  bfplem2  26547  grpokerinj  26575  divrngidl  26653  prnc  26692  prter2  26749  isnacs3  26785  pellexlem5  26918  pellex  26920  jm2.18  27081  jm2.15nn0  27096  jm2.16nn0  27097  setindtr  27117  dford3lem2  27120  ttac  27129  pmtrfrn  27400  psgnghm  27437  acsfn1p  27507  pm11.71  27596  ax10ext  27606  reuimrmo  27956  afvelima  28029  hbntal  28319  eel2221  28476  eel2122old  28497  bnj849  28957  bnj1110  29012  ax12-2  29103  ax12OLD  29105  a12study4  29117  a12study5rev  29122  ax10lem18ALT  29124  a12study  29132  a12study3  29135  a12study10  29136  a12study10n  29137  ax9lem2  29141  ax9lem13  29152  l1cvpat  29244  atcvrj0  29617  pmaple  29950  paddasslem5  30013  pclfinN  30089  osumcllem11N  30155  pexmidlem8N  30166  dvheveccl  31302  dihord6apre  31446  lpolconN  31677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator