MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5 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  1594  ax11w  1732  ax12dgen2  1737  ax5o  1761  spsd  1767  hbntOLD  1796  nfndOLD  1806  stdpc5OLD  1813  19.21hOLD  1858  cbv3hvOLD  1875  equs5e  1906  ax12olem1  1972  ax12olem1OLD  1977  ax12olem5OLD  1981  hbae  2005  a16gOLD  2013  dvelimh  2015  dvelimhOLD  2016  exdistrf  2028  ax11a2  2046  sbft  2074  sbied  2085  sb4  2102  ax11v  2145  ax11vALT  2146  ax5  2196  hbae-o  2203  dvelimf-o  2230  ax11indn  2245  ax11inda2  2249  ax11a2-o  2252  euimmo  2303  mopick  2316  spcimgft  2987  rr19.28v  3038  moeq3  3071  mob2  3074  euind  3081  reuind  3097  sbeqalb  3173  sbcimdv  3182  csbexg  3221  triun  4275  copsexg  4402  pwssun  4449  somo  4497  tz7.7  4567  ordunidif  4589  trsuc  4625  trsucss  4626  suc11  4644  reusv2lem2  4684  ralxfrd  4696  ralxfrALT  4701  onint  4734  limuni3  4791  tfi  4792  tfis  4793  tfinds  4798  limomss  4809  peano5  4827  relssres  5142  issref  5206  dmsnopg  5300  dfco2a  5329  imadif  5487  fvelima  5737  dffv2  5755  fvmptdf  5775  fvmptf  5780  fvmptnf  5781  foco2  5848  fconst5  5908  funfvima2  5933  funfvima3  5934  isores3  6014  oprabid  6064  ovmpt4g  6155  ovmpt2s  6156  ov2gf  6157  ovmpt2df  6164  suppss2  6259  suppssfv  6260  suppssov1  6261  fo2ndf  6412  frxp  6415  rntpos  6451  tposf2  6462  sorpsscmpl  6492  riotaxfrd  6540  riotasv3dOLD  6558  onfununi  6562  smofvon2  6577  smo11  6585  smoord  6586  tfrlem5  6600  tfrlem11  6608  tz7.44-2  6624  tz7.48lem  6657  tz7.48-1  6659  tz7.49  6661  tz7.49c  6662  omordi  6768  omord  6770  omass  6782  oneo  6783  omeulem1  6784  omopth2  6786  oewordri  6794  oeworde  6795  nnmordi  6833  nnmord  6834  omabs  6849  nnneo  6853  omsmo  6856  ectocld  6930  qsel  6942  eceqoveq  6968  mapsn  7014  f1oeng  7085  domunsncan  7167  sbthlem1  7176  2pwuninel  7221  mapen  7230  infensuc  7244  nneneq  7249  sucdom2  7262  pssnn  7286  dif1enOLD  7299  dif1en  7300  findcard2  7307  ac6sfi  7310  frfi  7311  unblem1  7318  unblem2  7319  unbnn2  7323  nnsdomg  7325  xpfi  7337  domunfican  7338  fiint  7342  fodomfi  7344  ixpfi2  7363  finsschain  7371  marypha1lem  7396  oiexg  7460  brwdom3  7506  sucprcreg  7523  inf3lem2  7540  inf3lem3  7541  noinfepOLD  7571  cantnfval2  7580  cantnflt  7583  cantnflem1  7601  cantnf  7605  cnfcom  7613  trcl  7620  epfrs  7623  r1sdom  7656  rankwflemb  7675  rankpwi  7705  rankelb  7706  carden2a  7809  cardsdomel  7817  carduni  7824  harval2  7840  pr2ne  7845  infpwfien  7899  cardaleph  7926  carduniima  7933  alephval3  7947  dfac5  7965  dfac12r  7982  dfac12k  7983  kmlem4  7989  kmlem11  7996  kmlem12  7997  cdainf  8028  infxp  8051  cfsuc  8093  cfcoflem  8108  coftr  8109  cfcof  8110  infpssr  8144  fin23lem30  8178  isf32lem1  8189  isf34lem6  8216  fin1a2lem13  8248  fin1a2s  8250  axcc2lem  8272  domtriomlem  8278  axdc4lem  8291  axcclem  8293  ac6num  8315  zorn2lem5  8336  zorn2lem6  8337  axdclem2  8356  alephval2  8403  alephreg  8413  pwcfsdom  8414  axpowndlem3  8430  axregndlem1  8433  axregnd  8435  axacndlem1  8438  axacndlem2  8439  axacndlem3  8440  axacndlem4  8441  axacnd  8443  gchi  8455  fpwwe2lem13  8473  canthp1  8485  gchpwdom  8505  wunfi  8552  tskwe2  8604  inar1  8606  gruen  8643  intgru  8645  indpi  8740  nqereu  8762  ltbtwnnq  8811  prnmadd  8830  genpcd  8839  prlem934  8866  ltexprlem1  8869  ltexprlem2  8870  ltexprlem7  8875  ltaprlem  8877  ltapr  8878  reclem4pr  8883  suplem2pr  8886  mulcmpblnr  8905  recexsrlem  8934  mulgt0sr  8936  recexsr  8938  supsrlem  8942  axpre-sup  9000  1re  9046  recex  9610  nnunb  10173  prime  10306  zeo  10311  fnn0ind  10325  zindd  10327  btwnz  10328  lbzbi  10520  xrub  10846  elfznelfzo  11147  facwordi  11535  fiinfnf1o  11589  hashclb  11596  hashdom  11608  hashf1lem2  11660  seqcoll  11667  limsupbnd2  12232  rlimdm  12300  o1of2  12361  rlimno1  12402  isercoll  12416  climcau  12419  caurcvg2  12426  caucvgb  12428  serf0  12429  zsum  12467  fsum2dlem  12509  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  incexclem  12571  odd2np1  12863  ndvdssub  12882  nprm  13048  maxprmfct  13068  rpexp  13075  pc2dvds  13207  pcfac  13223  unbenlem  13231  4sqlem12  13279  4sqlem17  13284  vdwlem6  13309  vdwlem13  13316  prmlem0  13383  xpscfv  13742  mreiincl  13776  sscfn1  13972  pospo  14385  cnvpsb  14600  dirref  14635  dirtr  14636  gaass  15029  elsymgbas  15052  cntz2ss  15086  odmulg  15147  odhash3  15165  sylow2alem1  15206  sylow2alem2  15207  pj1eu  15283  efgs1b  15323  efgsfo  15326  efgredlemc  15332  efgredeu  15339  frgpuptinv  15358  lt6abl  15459  ghmcyg  15460  ablfac1eulem  15585  pgpfac1lem5  15592  irredn1  15766  irredmul  15769  lspextmo  16087  lspsncv0  16173  mplcoe1  16483  mplcoe2  16485  cygth  16807  cnpco  17285  cnindis  17310  lmss  17316  lmcls  17320  lmcnp  17322  hausnei  17346  cmpsub  17417  tgcmp  17418  fiuncmp  17421  cmpfi  17425  1stcrest  17469  2ndcdisj  17472  1stccnp  17478  1stckgenlem  17538  txcls  17589  txcn  17611  txlm  17633  tx1stc  17635  txkgen  17637  xkococn  17645  hmphdis  17781  ptcmpfi  17798  isfild  17843  fgss2  17859  filcon  17868  trfil2  17872  ufileu  17904  filufint  17905  elfm2  17933  flftg  17981  cnpflf2  17985  fclssscls  18003  fclscf  18010  ufilcmp  18017  cnpfcf  18026  alexsubb  18030  alexsubALTlem4  18034  alexsubALT  18035  cnextcn  18051  divstgpopn  18102  tsmsxp  18137  isust  18186  xmettri2  18323  blin2  18412  setsmstopn  18461  met2ndc  18506  metcnp3  18523  tngtopn  18644  reconnlem2  18811  xrge0tsms  18818  fsumcn  18853  bndth  18936  iscmet3lem2  19198  iscmet3  19199  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ovolfiniun  19350  volfiniun  19394  ioombl1lem4  19408  dyadmbl  19445  ismbf3d  19499  itg1addlem4  19544  mbfi1flimlem  19567  itg2seq  19587  itgfsum  19671  ellimc3  19719  dvmptfsum  19812  c1liplem1  19833  evlseu  19890  plypf1  20084  plydivex  20167  aannenlem1  20198  ulmval  20249  ulmcau  20264  ulmss  20266  ulmbdd  20267  ulmcn  20268  ulmdvlem3  20271  pserulm  20291  sineq0  20382  efopn  20502  cxpeq  20594  rlimcnp  20757  xrlimcnp  20760  perfectlem2  20967  lgsdir2lem2  21061  lgsne0  21070  2sqlem6  21106  2sqlem10  21111  dchrisumlem2  21137  crcts  21562  cycls  21563  usgrcyclnl1  21580  4cycl4dv  21607  isgrpo  21737  grpoidinvlem3  21747  gxcom  21810  gxinv  21811  gxid  21814  gxdi  21837  opidon  21863  exidu1  21867  rngoideu  21925  rngodi  21926  rngodir  21927  rngmgmbs4  21958  rngoridfz  21976  vcdi  21984  vcdir  21985  vcass  21986  nvs  22104  nvtri  22112  blocnilem  22258  chintcli  22786  hsupss  22796  shlej1  22815  elspansn4  23028  spansncvi  23107  hoaddsub  23272  lnopl  23370  lnfnl  23387  riesz4i  23519  pjnormssi  23624  pj3si  23663  stlei  23696  stcltr2i  23731  dmdmd  23756  dmdbr5  23764  mdslmd1lem2  23782  atssma  23834  atcvatlem  23841  chirredlem1  23846  atcvat4i  23853  mdsymlem2  23860  mdsymlem6  23864  sumdmdlem2  23875  dmdbr5ati  23878  cdjreui  23888  elimifd  23957  disjxpin  23981  suppss2f  24002  xrge0tsmsd  24176  lmxrge0  24290  ismeas  24506  conpcon  24875  cvmseu  24916  cvmliftlem15  24938  cvmlift2lem1  24942  cvmlift2lem12  24954  ghomf1olem  25058  dedekindle  25141  zprod  25216  fprod2dlem  25257  fprod2d  25258  dfpo2  25326  fundmpss  25336  dfon2lem3  25355  dfon2lem4  25356  dfon2lem6  25358  dfon2lem8  25360  dfon2lem9  25361  hbntg  25376  tfisg  25418  wfisg  25423  dftrpred3g  25450  trpredrec  25455  frinsg  25459  soseq  25468  wfr3g  25469  wfrlem4  25473  wfrlem5  25474  frr3g  25494  frrlem4  25498  frrlem5  25499  sltval2  25524  nodenselem5  25553  axlowdimlem16  25800  axcontlem2  25808  cgrdegen  25842  funtransport  25869  ifscgr  25882  cgrxfr  25893  brofs2  25915  brifs2  25916  idinside  25922  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn1lem14  25938  broutsideof2  25960  btwnoutside  25963  outsideoftr  25967  ontgval  26085  ordtop  26090  ordcmp  26101  onint1  26103  wl-bitr1  26124  voliunnfl  26149  volsupnfl  26150  itg2addnclem2  26156  itg2addnc  26158  itg2gt0cn  26159  finminlem  26211  ntruni  26220  comppfsc  26277  neibastop1  26278  filbcmb  26332  sdclem2  26336  seqpo  26341  nninfnub  26345  neificl  26349  prdstotbnd  26393  cnpwstotbnd  26396  heibor1lem  26408  heibor  26420  bfplem2  26422  grpokerinj  26450  divrngidl  26528  prnc  26567  prter2  26620  isnacs3  26654  pellexlem5  26786  pellex  26788  jm2.18  26949  jm2.15nn0  26964  jm2.16nn0  26965  setindtr  26985  dford3lem2  26988  ttac  26997  pmtrfrn  27268  psgnghm  27305  acsfn1p  27375  pm11.71  27464  ax10ext  27474  reuimrmo  27823  afvelima  27898  rlimdmafv  27908  0mnnnnn0  27971  el2wlkonot  28066  2wlkonot3v  28072  2spthonot3v  28073  2pthfrgra  28115  hbntal  28351  eel2221  28513  eel2122old  28537  bnj849  29002  bnj1110  29057  hbaewAUX7  29184  dvelimhvAUX7  29198  exdistrfNEW7  29211  ax11a2NEW7  29235  sbiedNEW7  29244  a16gNEW7  29250  sb4NEW7  29256  sbftNEW7  29260  ax11vNEW7  29296  hbaew0AUX7  29347  hbaew4AUX7  29348  hbaeOLD7  29392  dvelimhOLD7  29397  l1cvpat  29537  atcvrj0  29910  pmaple  30243  paddasslem5  30306  pclfinN  30382  osumcllem11N  30448  pexmidlem8N  30459  dvheveccl  31595  dihord6apre  31739  lpolconN  31970
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator