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  1587  ax11w  1721  ax12dgen2  1726  ax5o  1750  spsd  1756  hbnt  1776  nfndOLD  1793  stdpc5OLD  1800  19.21hOLD  1845  cbv3hvOLD  1856  equs5e  1892  ax12olem5  1936  a16g  1950  hbae  1958  dvelimh  1969  exdistrf  1976  ax11a2  1998  sbft  2030  sbied  2041  sb4  2058  ax11v  2101  ax11vALT  2102  ax5  2151  hbae-o  2158  dvelimf-o  2185  ax11indn  2200  ax11inda2  2204  ax11a2-o  2207  euimmo  2258  mopick  2271  spcimgft  2935  rr19.28v  2986  moeq3  3018  mob2  3021  euind  3028  reuind  3044  sbeqalb  3119  sbcimdv  3128  csbexg  3167  triun  4207  copsexg  4334  pwssun  4381  somo  4430  tz7.7  4500  ordunidif  4522  trsuc  4558  trsuc2OLD  4559  trsucss  4560  suc11  4578  reusv2lem2  4618  ralxfrd  4630  ralxfrALT  4635  onint  4668  limuni3  4725  tfi  4726  tfis  4727  tfinds  4732  limomss  4743  peano5  4761  relssres  5074  issref  5138  dmsnopg  5226  dfco2a  5255  imadif  5409  fvelima  5657  dffv2  5675  fvmptdf  5694  fvmptf  5699  fvmptnf  5700  foco2  5763  fconst5  5815  funfvima2  5840  funfvima3  5841  isores3  5919  oprabid  5969  ovmpt4g  6057  ovmpt2s  6058  ov2gf  6059  ovmpt2df  6066  suppss2  6160  suppssfv  6161  suppssov1  6162  frxp  6312  rntpos  6334  tposf2  6345  sorpsscmpl  6375  riotaxfrd  6423  riotasv3dOLD  6441  onfununi  6445  smofvon2  6460  smo11  6468  smoord  6469  tfrlem5  6483  tfrlem11  6491  tz7.44-2  6507  tz7.48lem  6540  tz7.48-1  6542  tz7.49  6544  tz7.49c  6545  omordi  6651  omord  6653  omass  6665  oneo  6666  omeulem1  6667  omopth2  6669  oewordri  6677  oeworde  6678  nnmordi  6716  nnmord  6717  omabs  6732  nnneo  6736  omsmo  6739  ectocld  6813  qsel  6825  eceqoveq  6851  mapsn  6897  f1oeng  6968  domunsncan  7050  sbthlem1  7059  2pwuninel  7104  mapen  7113  infensuc  7127  nneneq  7132  sucdom2  7145  pssnn  7169  dif1enOLD  7180  dif1en  7181  findcard2  7188  ac6sfi  7191  frfi  7192  unblem1  7199  unblem2  7200  unbnn2  7204  nnsdomg  7206  xpfi  7218  domunfican  7219  fiint  7223  fodomfi  7225  ixpfi2  7244  finsschain  7252  marypha1lem  7276  oiexg  7340  brwdom3  7386  sucprcreg  7403  inf3lem2  7420  inf3lem3  7421  noinfepOLD  7451  cantnfval2  7460  cantnflt  7463  cantnflem1  7481  cantnf  7485  cnfcom  7493  trcl  7500  epfrs  7503  r1sdom  7536  rankwflemb  7555  rankpwi  7585  rankelb  7586  carden2a  7689  cardsdomel  7697  carduni  7704  harval2  7720  pr2ne  7725  infpwfien  7779  cardaleph  7806  carduniima  7813  alephval3  7827  dfac5  7845  dfac12r  7862  dfac12k  7863  kmlem4  7869  kmlem11  7876  kmlem12  7877  cdainf  7908  infxp  7931  cfsuc  7973  cfcoflem  7988  coftr  7989  cfcof  7990  infpssr  8024  fin23lem30  8058  isf32lem1  8069  isf34lem6  8096  fin1a2lem13  8128  fin1a2s  8130  axcc2lem  8152  domtriomlem  8158  axdc4lem  8171  axcclem  8173  ac6num  8196  zorn2lem5  8217  zorn2lem6  8218  axdclem2  8237  alephval2  8284  alephreg  8294  pwcfsdom  8295  axpowndlem3  8311  axregndlem1  8314  axregnd  8316  axacndlem1  8319  axacndlem2  8320  axacndlem3  8321  axacndlem4  8322  axacnd  8324  gchi  8336  fpwwe2lem13  8354  canthp1  8366  gchpwdom  8386  wunfi  8433  tskwe2  8485  inar1  8487  gruen  8524  intgru  8526  indpi  8621  nqereu  8643  ltbtwnnq  8692  prnmadd  8711  genpcd  8720  prlem934  8747  ltexprlem1  8750  ltexprlem2  8751  ltexprlem7  8756  ltaprlem  8758  ltapr  8759  reclem4pr  8764  suplem2pr  8767  mulcmpblnr  8786  recexsrlem  8815  mulgt0sr  8817  recexsr  8819  supsrlem  8823  axpre-sup  8881  1re  8927  recex  9490  nnunb  10053  prime  10184  zeo  10189  fnn0ind  10203  zindd  10205  btwnz  10206  lbzbi  10398  xrub  10722  facwordi  11395  hashclb  11445  hashdom  11454  hashf1lem2  11490  seqcoll  11497  limsupbnd2  12053  rlimdm  12121  o1of2  12182  rlimno1  12223  isercoll  12237  climcau  12240  caurcvg2  12247  caucvgb  12249  serf0  12250  zsum  12288  fsum2dlem  12330  fsum2d  12331  fsumabs  12356  fsumrlim  12366  fsumo1  12367  fsumiun  12376  incexclem  12392  odd2np1  12684  ndvdssub  12703  nprm  12869  maxprmfct  12889  rpexp  12896  pc2dvds  13028  pcfac  13044  unbenlem  13052  4sqlem12  13100  4sqlem17  13105  vdwlem6  13130  vdwlem13  13137  prmlem0  13204  xpscfv  13563  mreiincl  13597  catpropd  13711  sscfn1  13793  pospo  14206  cnvpsb  14421  dirref  14456  dirtr  14457  gaass  14850  elsymgbas  14873  cntz2ss  14907  odmulg  14968  odhash3  14986  sylow2alem1  15027  sylow2alem2  15028  pj1eu  15104  efgs1b  15144  efgsfo  15147  efgredlemc  15153  efgredeu  15160  frgpuptinv  15179  lt6abl  15280  ghmcyg  15281  ablfac1eulem  15406  pgpfac1lem5  15413  irredn1  15587  irredmul  15590  lspextmo  15912  lspsncv0  15998  mplcoe1  16308  mplcoe2  16310  cygth  16631  cnpco  17102  cnindis  17126  lmss  17132  lmcls  17136  lmcnp  17138  hausnei  17162  cmpsub  17233  tgcmp  17234  fiuncmp  17237  cmpfi  17241  1stcrest  17285  2ndcdisj  17288  1stccnp  17294  1stckgenlem  17354  txcls  17405  txcn  17426  txlm  17448  tx1stc  17450  txkgen  17452  xkococn  17460  hmphdis  17593  ptcmpfi  17610  isfild  17655  fgss2  17671  filcon  17680  trfil2  17684  ufileu  17716  filufint  17717  elfm2  17745  flftg  17793  cnpflf2  17797  fclssscls  17815  fclscf  17822  ufilcmp  17829  cnpfcf  17838  alexsubb  17842  alexsubALTlem4  17846  alexsubALT  17847  divstgpopn  17904  tsmsxp  17939  xmettri2  18007  blin2  18077  setsmstopn  18126  met2ndc  18171  metcnp3  18188  tngtopn  18268  reconnlem2  18435  xrge0tsms  18442  fsumcn  18477  bndth  18560  iscmet3lem2  18822  iscmet3  18823  ivthlem1  18915  ivthlem2  18916  ivthlem3  18917  ovolfiniun  18964  volfiniun  19008  ioombl1lem4  19022  dyadmbl  19059  ismbf3d  19113  itg1addlem4  19158  mbfi1flimlem  19181  itg2seq  19201  itgfsum  19285  ellimc3  19333  dvmptfsum  19426  c1liplem1  19447  evlseu  19504  plypf1  19698  plydivex  19781  aannenlem1  19812  ulmval  19863  ulmcau  19878  ulmss  19880  ulmbdd  19881  ulmcn  19882  ulmdvlem3  19885  pserulm  19905  sineq0  19996  efopn  20116  cxpeq  20208  rlimcnp  20371  xrlimcnp  20374  perfectlem2  20581  lgsdir2lem2  20675  lgsne0  20684  2sqlem6  20720  2sqlem10  20725  dchrisumlem2  20751  isgrpo  20975  grpoidinvlem3  20985  gxcom  21048  gxinv  21049  gxid  21052  gxdi  21075  opidon  21101  exidu1  21105  rngoideu  21163  rngodi  21164  rngodir  21165  rngmgmbs4  21196  rngoridfz  21214  vcdi  21222  vcdir  21223  vcass  21224  nvs  21342  nvtri  21350  blocnilem  21496  chintcli  22024  hsupss  22034  shlej1  22053  elspansn4  22266  spansncvi  22345  hoaddsub  22510  lnopl  22608  lnfnl  22625  riesz4i  22757  pjnormssi  22862  pj3si  22901  stlei  22934  stcltr2i  22969  dmdmd  22994  dmdbr5  23002  mdslmd1lem2  23020  atssma  23072  atcvatlem  23079  chirredlem1  23084  atcvat4i  23091  mdsymlem2  23098  mdsymlem6  23102  sumdmdlem2  23113  dmdbr5ati  23116  cdjreui  23126  elimifd  23203  suppss2f  23253  xrge0tsmsd  23415  unitdivcld  23455  lmxrge0  23493  cnextcn  23504  isust  23509  ismeas  23819  conpcon  24170  cvmseu  24211  cvmliftlem15  24233  cvmlift2lem1  24237  cvmlift2lem12  24249  ghomf1olem  24405  dedekindle  24489  zprod  24564  dfpo2  24670  fundmpss  24680  dfon2lem3  24699  dfon2lem4  24700  dfon2lem6  24702  dfon2lem8  24704  dfon2lem9  24705  hbntg  24720  tfisg  24762  wfisg  24767  dftrpred3g  24794  trpredrec  24799  frinsg  24803  soseq  24812  wfr3g  24813  wfrlem4  24817  wfrlem5  24818  frr3g  24838  frrlem4  24842  frrlem5  24843  sltval2  24868  nodenselem5  24897  axlowdimlem16  25144  axcontlem2  25152  cgrdegen  25186  funtransport  25213  ifscgr  25226  cgrxfr  25237  brofs2  25259  brifs2  25260  idinside  25266  btwnconn1lem7  25275  btwnconn1lem11  25279  btwnconn1lem12  25280  btwnconn1lem14  25282  broutsideof2  25304  btwnoutside  25307  outsideoftr  25311  ontgval  25429  ordtop  25434  ordcmp  25445  onint1  25447  wl-bitr1  25469  voliunnfl  25490  volsupnfl  25491  itg2addnclem2  25493  itg2addnc  25494  itg2gt0cn  25495  finminlem  25555  ntruni  25569  comppfsc  25631  neibastop1  25632  filbcmb  25756  sdclem2  25776  seqpo  25781  nninfnub  25785  neificl  25791  prdstotbnd  25841  cnpwstotbnd  25844  heibor1lem  25856  heibor  25868  bfplem2  25870  grpokerinj  25898  divrngidl  25976  prnc  26015  prter2  26072  isnacs3  26108  pellexlem5  26241  pellex  26243  jm2.18  26404  jm2.15nn0  26419  jm2.16nn0  26420  setindtr  26440  dford3lem2  26443  ttac  26452  pmtrfrn  26723  psgnghm  26760  acsfn1p  26830  pm11.71  26919  ax10ext  26929  reuimrmo  27279  afvelima  27355  rlimdmafv  27365  elfznelfzo  27462  fiinfnf1o  27482  crcts  27745  cycls  27746  usgrcyclnl1  27764  4cycl4dv  27791  hbntal  28064  eel2221  28227  eel2122old  28251  bnj849  28719  bnj1110  28774  cbv3hvNEW7  28869  hbaewAUX7  28901  dvelimhvAUX7  28915  exdistrfNEW7  28928  ax11a2NEW7  28952  sbiedNEW7  28961  a16gNEW7  28967  sb4NEW7  28973  sbftNEW7  28977  ax11vNEW7  29013  hbaew0AUX7  29064  ax7w2AUX7  29067  ax7w7tAUX7  29073  hbaeOLD7  29109  dvelimhOLD7  29114  ax12-2  29172  ax12OLD  29174  a12study4  29186  a12study5rev  29191  ax10lem18ALT  29193  a12study  29201  a12study3  29204  a12study10  29205  a12study10n  29206  ax9lem2  29210  ax9lem13  29221  l1cvpat  29313  atcvrj0  29686  pmaple  30019  paddasslem5  30082  pclfinN  30158  osumcllem11N  30224  pexmidlem8N  30235  dvheveccl  31371  dihord6apre  31515  lpolconN  31746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator