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  1577  ax11w  1707  ax12dgen2  1712  ax5o  1729  hbnt  1736  19.21h  1743  cbv3hv  1749  spsd  1752  nfnd  1772  stdpc5  1805  ax12olem5  1884  a16g  1898  hbae  1906  dvelimh  1917  exdistrf  1924  ax11a2  1946  sbft  1978  sbied  1989  sb4  2006  ax11v  2049  ax5  2098  hbae-o  2105  dvelimf-o  2132  ax11indn  2147  ax11inda2  2151  ax11a2-o  2154  euimmo  2205  mopick  2218  spcimgft  2872  rr19.28v  2923  moeq3  2955  mob2  2958  euind  2965  reuind  2981  sbeqalb  3056  sbcimdv  3065  csbexg  3104  triun  4142  copsexg  4268  pwssun  4315  somo  4364  tz7.7  4434  ordunidif  4456  trsuc  4492  trsuc2OLD  4493  trsucss  4494  suc11  4512  reusv2lem2  4552  ralxfrd  4564  ralxfrALT  4569  onint  4602  limuni3  4659  tfi  4660  tfis  4661  tfinds  4666  limomss  4677  peano5  4695  relssres  5008  issref  5072  dmsnopg  5160  dfco2a  5189  imadif  5343  fvelima  5590  dffv2  5608  fvmptdf  5627  fvmptf  5632  fvmptnf  5633  foco2  5696  fconst5  5747  funfvima2  5770  funfvima3  5771  isores3  5848  oprabid  5898  ovmpt4g  5986  ovmpt2s  5987  ov2gf  5988  ovmpt2df  5995  suppss2  6089  suppssfv  6090  suppssov1  6091  frxp  6241  rntpos  6263  tposf2  6274  sorpsscmpl  6304  riotaxfrd  6352  riotasv3dOLD  6370  onfununi  6374  smofvon2  6389  smo11  6397  smoord  6398  tfrlem5  6412  tfrlem11  6420  tz7.44-2  6436  tz7.48lem  6469  tz7.48-1  6471  tz7.49  6473  tz7.49c  6474  omordi  6580  omord  6582  omass  6594  oneo  6595  omeulem1  6596  omopth2  6598  oewordri  6606  oeworde  6607  nnmordi  6645  nnmord  6646  omabs  6661  nnneo  6665  omsmo  6668  ectocld  6742  qsel  6754  eceqoveq  6779  mapsn  6825  f1oeng  6896  domunsncan  6978  sbthlem1  6987  2pwuninel  7032  mapen  7041  infensuc  7055  nneneq  7060  sucdom2  7073  pssnn  7097  dif1enOLD  7106  dif1en  7107  findcard2  7114  ac6sfi  7117  frfi  7118  unblem1  7125  unblem2  7126  unbnn2  7130  nnsdomg  7132  xpfi  7144  domunfican  7145  fiint  7149  fodomfi  7151  ixpfi2  7170  finsschain  7178  marypha1lem  7202  oiexg  7266  brwdom3  7312  sucprcreg  7329  inf3lem2  7346  inf3lem3  7347  noinfepOLD  7377  cantnfval2  7386  cantnflt  7389  cantnflem1  7407  cantnf  7411  cnfcom  7419  trcl  7426  epfrs  7429  r1sdom  7462  rankwflemb  7481  rankpwi  7511  rankelb  7512  carden2a  7615  cardsdomel  7623  carduni  7630  harval2  7646  pr2ne  7651  infpwfien  7705  cardaleph  7732  carduniima  7739  alephval3  7753  dfac5  7771  dfac12r  7788  dfac12k  7789  kmlem4  7795  kmlem11  7802  kmlem12  7803  cdainf  7834  infxp  7857  cfsuc  7899  cfcoflem  7914  coftr  7915  cfcof  7916  infpssr  7950  fin23lem30  7984  isf32lem1  7995  isf34lem6  8022  fin1a2lem13  8054  fin1a2s  8056  axcc2lem  8078  domtriomlem  8084  axdc4lem  8097  axcclem  8099  ac6num  8122  zorn2lem5  8143  zorn2lem6  8144  axdclem2  8163  alephval2  8210  alephreg  8220  pwcfsdom  8221  axpowndlem3  8237  axregndlem1  8240  axregnd  8242  axacndlem1  8245  axacndlem2  8246  axacndlem3  8247  axacndlem4  8248  axacnd  8250  gchi  8262  fpwwe2lem13  8280  canthp1  8292  gchpwdom  8312  wunfi  8359  tskwe2  8411  inar1  8413  gruen  8450  intgru  8452  indpi  8547  nqereu  8569  ltbtwnnq  8618  prnmadd  8637  genpcd  8646  prlem934  8673  ltexprlem1  8676  ltexprlem2  8677  ltexprlem7  8682  ltaprlem  8684  ltapr  8685  reclem4pr  8690  suplem2pr  8693  mulcmpblnr  8712  recexsrlem  8741  mulgt0sr  8743  recexsr  8745  supsrlem  8749  axpre-sup  8807  1re  8853  recex  9416  nnunb  9977  prime  10108  zeo  10113  fnn0ind  10127  zindd  10129  btwnz  10130  lbzbi  10322  xrub  10646  facwordi  11318  hashclb  11368  hashdom  11377  hashf1lem2  11410  seqcoll  11417  limsupbnd2  11973  rlimdm  12041  o1of2  12102  rlimno1  12143  isercoll  12157  climcau  12160  caurcvg2  12166  caucvgb  12168  serf0  12169  zsum  12207  fsum2dlem  12249  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  incexclem  12311  odd2np1  12603  ndvdssub  12622  nprm  12788  maxprmfct  12808  rpexp  12815  pc2dvds  12947  pcfac  12963  unbenlem  12971  4sqlem12  13019  4sqlem17  13024  vdwlem6  13049  vdwlem13  13056  prmlem0  13123  xpscfv  13480  mreiincl  13514  catpropd  13628  sscfn1  13710  pospo  14123  cnvpsb  14338  dirref  14373  dirtr  14374  gaass  14767  elsymgbas  14790  cntz2ss  14824  odmulg  14885  odhash3  14903  sylow2alem1  14944  sylow2alem2  14945  pj1eu  15021  efgs1b  15061  efgsfo  15064  efgredlemc  15070  efgredeu  15077  frgpuptinv  15096  lt6abl  15197  ghmcyg  15198  ablfac1eulem  15323  pgpfac1lem5  15330  irredn1  15504  irredmul  15507  lspextmo  15829  lspsncv0  15915  mplcoe1  16225  mplcoe2  16227  cygth  16541  cnpco  17012  cnindis  17036  lmss  17042  lmcls  17046  lmcnp  17048  hausnei  17072  cmpsub  17143  tgcmp  17144  fiuncmp  17147  cmpfi  17151  1stcrest  17195  2ndcdisj  17198  1stccnp  17204  1stckgenlem  17264  txcls  17315  txcn  17336  txlm  17358  tx1stc  17360  txkgen  17362  xkococn  17370  hmphdis  17503  ptcmpfi  17520  isfild  17569  fgss2  17585  filcon  17594  trfil2  17598  ufileu  17630  filufint  17631  elfm2  17659  flftg  17707  cnpflf2  17711  fclssscls  17729  fclscf  17736  ufilcmp  17743  cnpfcf  17752  alexsubb  17756  alexsubALTlem4  17760  alexsubALT  17761  divstgpopn  17818  tsmsxp  17853  xmettri2  17921  blin2  17991  setsmstopn  18040  met2ndc  18085  metcnp3  18102  tngtopn  18182  reconnlem2  18348  xrge0tsms  18355  fsumcn  18390  bndth  18472  iscmet3lem2  18734  iscmet3  18735  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  ovolfiniun  18876  volfiniun  18920  ioombl1lem4  18934  dyadmbl  18971  ismbf3d  19025  itg1addlem4  19070  mbfi1flimlem  19093  itg2seq  19113  itgfsum  19197  ellimc3  19245  dvmptfsum  19338  c1liplem1  19359  evlseu  19416  plypf1  19610  plydivex  19693  aannenlem1  19724  ulmval  19775  ulmcau  19788  ulmss  19790  ulmbdd  19791  ulmcn  19792  ulmdvlem3  19795  pserulm  19814  sineq0  19905  efopn  20021  cxpeq  20113  rlimcnp  20276  xrlimcnp  20279  perfectlem2  20485  lgsdir2lem2  20579  lgsne0  20588  2sqlem6  20624  2sqlem10  20629  dchrisumlem2  20655  isgrpo  20879  grpoidinvlem3  20889  gxcom  20952  gxinv  20953  gxid  20956  gxdi  20979  opidon  21005  exidu1  21009  rngoideu  21067  rngodi  21068  rngodir  21069  rngmgmbs4  21100  vcdi  21124  vcdir  21125  vcass  21126  nvs  21244  nvtri  21252  blocnilem  21398  chintcli  21926  hsupss  21936  shlej1  21955  elspansn4  22168  spansncvi  22247  hoaddsub  22412  lnopl  22510  lnfnl  22527  riesz4i  22659  pjnormssi  22764  pj3si  22803  stlei  22836  stcltr2i  22871  dmdmd  22896  dmdbr5  22904  mdslmd1lem2  22922  atssma  22974  atcvatlem  22981  chirredlem1  22986  atcvat4i  22993  mdsymlem2  23000  mdsymlem6  23004  sumdmdlem2  23015  dmdbr5ati  23018  cdjreui  23028  elimifd  23167  suppss2f  23216  unitdivcld  23300  lmxrge0  23390  xrge0tsmsd  23397  ismeas  23545  conpcon  23781  cvmseu  23822  cvmliftlem15  23844  cvmlift2lem1  23848  cvmlift2lem12  23860  ghomf1olem  24016  dedekindle  24098  zprod  24160  dfpo2  24183  fundmpss  24193  dfon2lem3  24212  dfon2lem4  24213  dfon2lem6  24215  dfon2lem8  24217  dfon2lem9  24218  hbntg  24233  tfisg  24275  wfisg  24280  dftrpred3g  24307  trpredrec  24312  frinsg  24316  soseq  24325  wfr3g  24326  wfrlem4  24330  wfrlem5  24331  frr3g  24351  frrlem4  24355  frrlem5  24356  sltval2  24381  nodenselem5  24410  axlowdimlem16  24657  axcontlem2  24665  cgrdegen  24699  funtransport  24726  ifscgr  24739  cgrxfr  24750  brofs2  24772  brifs2  24773  idinside  24779  btwnconn1lem7  24788  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn1lem14  24795  broutsideof2  24817  btwnoutside  24820  outsideoftr  24824  ontgval  24942  ordtop  24947  ordcmp  24958  onint1  24960  wl-bitr1  24982  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  untind  25121  prl2  25272  domrancur1c  25305  valcurfn1  25307  rngoridfz  25540  intopcoaconlem3b  25641  hdrmp  25809  cmpassoh  25904  cmpmon  25918  idmon  25920  iepiclem  25926  propsrc  25971  finminlem  26334  ntruni  26348  comppfsc  26410  neibastop1  26411  filbcmb  26535  sdclem2  26555  seqpo  26560  nninfnub  26564  neificl  26570  prdstotbnd  26621  cnpwstotbnd  26624  heibor1lem  26636  heibor  26648  bfplem2  26650  grpokerinj  26678  divrngidl  26756  prnc  26795  prter2  26852  isnacs3  26888  pellexlem5  27021  pellex  27023  jm2.18  27184  jm2.15nn0  27199  jm2.16nn0  27200  setindtr  27220  dford3lem2  27223  ttac  27232  pmtrfrn  27503  psgnghm  27540  acsfn1p  27610  pm11.71  27699  ax10ext  27709  reuimrmo  28059  afvelima  28135  rlimdmafv  28145  elfznelfzo  28213  crcts  28367  cycls  28368  usgrcyclnl1  28386  4cycl4dv  28413  hbntal  28618  eel2221  28781  eel2122old  28805  bnj849  29273  bnj1110  29328  cbv3hvNEW7  29423  hbaewAUX7  29455  dvelimhvAUX7  29469  exdistrfNEW7  29482  ax11a2NEW7  29506  sbiedNEW7  29515  a16gNEW7  29521  sb4NEW7  29527  sbftNEW7  29531  ax11vNEW7  29567  hbaew0AUX7  29617  ax7w2AUX7  29620  ax7w7tAUX7  29626  hbaeOLD7  29662  dvelimhOLD7  29667  ax12-2  29725  ax12OLD  29727  a12study4  29739  a12study5rev  29744  ax10lem18ALT  29746  a12study  29754  a12study3  29757  a12study10  29758  a12study10n  29759  ax9lem2  29763  ax9lem13  29774  l1cvpat  29866  atcvrj0  30239  pmaple  30572  paddasslem5  30635  pclfinN  30711  osumcllem11N  30777  pexmidlem8N  30788  dvheveccl  31924  dihord6apre  32068  lpolconN  32299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator