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

Theorem syld 42
Description: Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Notice that syld 42 has the same form as syl 17 with  ph added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace  ph with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 21 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible.

Hypotheses
Ref Expression
syld.1  |-  ( ph  ->  ( ps  ->  ch ) )
syld.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
syld  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syld
StepHypRef Expression
1 syld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syld.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
32a1d 24 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpdd 38 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  3syld  53  sylsyld  54  nsyld  134  pm2.61d  152  sylibd  207  sylbid  208  sylibrd  227  sylbird  228  syland  469  ax10lem23  1672  ax10lem24  1673  alrimdd  1709  dral1  1855  dral1-o  1856  cbv1h  1870  sbied  1908  sbequi  1951  ax11indalem  2110  ax11inda2ALT  2111  trel3  4018  poss  4209  sess2  4255  wefrc  4280  wereu2  4283  ordelord  4307  oninton  4482  orduniorsuc  4512  limuni3  4534  tfindsg  4542  limom  4562  funun  5153  ssimaex  5436  f1dmex  5603  f1imass  5640  soisoi  5677  isores3  5684  isofrlem  5689  isoselem  5690  weniso  5704  soxp  6080  riotasv3dOLD  6240  smoel  6263  smogt  6270  tfrlem9  6287  tz7.49  6343  seqomlem1  6348  abianfp  6357  odi  6463  omass  6464  omeulem2  6467  oeordsuc  6478  oeeulem  6485  ertr  6561  swoord2  6576  ecopovtrn  6647  domtriord  6892  2pwuninel  6901  onomeneq  6935  unxpdomlem2  6953  isinf  6961  pssnn  6966  findcard3  6985  frfi  6987  unblem3  6996  dffi3  7068  inf3lem3  7215  inf3lem5  7217  noinfep  7244  cantnfle  7256  cantnfp1lem3  7266  en3lplem1  7300  rankxpsuc  7436  tcrank  7438  ficardom  7478  carduni  7498  infxpenlem  7525  dfac8alem  7540  ac10ct  7545  ween  7546  alephdom  7592  alephle  7599  iscard3  7604  alephfp  7619  cdainf  7702  pwsdompw  7714  infdif  7719  cfslbn  7777  cofsmo  7779  cfsmolem  7780  cfcof  7784  fin1a2s  7924  domtriomlem  7952  ac6num  7990  zorn2lem3  8009  axdclem2  8031  imadomg  8043  iundom2g  8046  ficard  8069  fpwwe2lem8  8139  fpwwe2  8145  gchaclem  8172  tskr1om2  8270  inar1  8277  tskord  8282  tskuni  8285  grudomon  8319  grur1a  8321  grur1  8322  addnidpi  8405  ltexnq  8479  genpnnp  8509  addclprlem2  8521  mulclprlem  8523  psslinpr  8535  ltaddpr2  8539  ltexprlem6  8545  ltexprlem7  8546  addcanpr  8550  mulgt0sr  8607  map2psrpr  8612  supsrlem  8613  axrrecex  8665  letr  8794  recex  9280  lemul12b  9493  mulgt1  9495  ledivmulOLD  9510  fimaxre2  9582  lbreu  9584  nnrecgt0  9663  nnunb  9840  bndndx  9843  zeo  9976  uzind  9982  fzind  9988  fnn0ind  9989  lbzbi  10185  suprzcl2  10187  zmax  10192  rpnnen1lem5  10225  xrletr  10368  qbtwnre  10404  qsqueeze  10406  qextltlem  10407  xralrple  10410  xlesubadd  10461  supxrunb1  10516  icoshft  10636  fzen  10689  modadd1  10879  modmul1  10880  uzrdgfni  10899  seqcl2  10942  seqfveq2  10946  seqshft2  10950  monoord  10954  seqsplit  10957  seqf1olem1  10963  seqf1olem2  10964  seqid2  10970  seqhomo  10971  expnbnd  11108  faclbnd4lem4  11187  seqcoll  11278  sqeqd  11528  sqrmo  11614  cau3lem  11715  limsupbnd2  11834  lo1bdd2  11875  climuni  11903  rlimcn2  11941  mulcn2  11946  o1of2  11963  rlimo1  11967  lo1le  12002  isercolllem1  12015  iseralt  12034  isumrpcl  12176  cvgrat  12213  rpnnen2  12378  ruclem3  12385  sqr2irr  12401  dvds2lem  12415  dvdslelem  12447  divalglem8  12473  bitsinv1lem  12506  sadcaddlem  12522  smu01lem  12550  smueqlem  12555  bezoutlem4  12594  algcvga  12623  isprm3  12641  coprm  12653  coprmdvds2  12656  isprm5  12665  rpexp12i  12675  phibndlem  12712  dfphi2  12716  eulerthlem2  12724  odzdvds  12734  iserodd  12762  pclem  12765  pcpremul  12770  pcqcl  12783  pcdvdsb  12795  pcprmpw2  12808  pcaddlem  12810  pcmptcl  12813  pcfac  12821  prmpwdvds  12825  unbenlem  12829  prmreclem1  12837  4sqlem17  12882  vdwmc2  12900  vdwlem9  12910  vdwlem10  12911  vdwlem13  12914  vdwnnlem3  12918  ramcl  12950  mreiincl  13370  pospo  13951  dirge  14194  oddvdsnn0  14694  oddvds  14697  odcl2  14713  gexdvds  14730  sylow1lem1  14744  sylow2alem2  14764  sylow2a  14765  efgi2  14869  efgsrel  14878  efgs1b  14880  cyggex2  15018  pgpfac1lem2  15145  pgpfac1lem3a  15146  pgpfac1lem3  15147  pgpfac1lem5  15149  lssssr  15545  gzrngunitlem  16268  znunit  16349  frgpcyg  16359  lsmcss  16424  obselocv  16460  obslbs  16462  ordtrest2lem  16765  leordtval2  16774  lecldbas  16781  cncls  16835  cncnp  16841  cnpresti  16848  lmcnp  16864  cnt0  16906  isreg2  16937  cmpsublem  16958  cmpsub  16959  tgcmp  16960  dfcon2  16977  1stcfb  17003  2ndcctbss  17013  1stcelcls  17019  islly2  17042  dislly  17055  kgencn2  17084  txcnp  17146  txindis  17160  txcmplem1  17167  txlm  17174  xkohaus  17179  cnmptcom  17204  kqfvima  17253  isr0  17260  fgss2  17401  fbasrn  17411  filuni  17412  ufilmax  17434  isufil2  17435  cfinufil  17455  fmfnfmlem1  17481  fmfnfmlem2  17482  fmfnfmlem4  17484  fmfnfm  17485  fmco  17488  flimopn  17502  hausflim  17508  flimrest  17510  fclsopn  17541  flimfnfcls  17555  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALT  17577  ptcmplem2  17579  symgtgp  17616  divstgplem  17635  tsmsres  17658  tsmsxplem1  17667  imasdsf1olem  17769  bldisj  17787  blss  17804  metcnp3  17918  ngptgp  17984  nrginvrcn  18034  nmoleub  18072  xrsmopn  18150  icccmplem3  18161  reconnlem2  18164  rectbntr0  18169  rescncf  18233  icoopnst  18269  iocopnst  18270  iccpnfcnv  18274  lebnumii  18296  nmoleub2lem  18427  nmhmcn  18433  fgcfil  18529  iscfil3  18531  iscau2  18535  iscau3  18536  iscau4  18537  iscmet3lem2  18550  cfilres  18554  caussi  18555  equivcfil  18557  equivcau  18558  caubl  18565  ivthlem2  18644  ivthlem3  18645  ovoliunlem2  18694  ovoliunnul  18698  ovolicc2lem3  18710  ioombl1lem4  18750  dyadmax  18785  dyadmbl  18787  volsup2  18792  itg2le  18926  itg2const2  18928  itg2seq  18929  itgsplitioo  19024  dvnres  19112  rolle  19169  c1lip1  19176  dvivthlem1  19187  lhop1  19193  dvcnvrelem1  19196  dvfsumrlim  19210  ply1divmo  19353  ig1peu  19389  plypf1  19426  coeaddlem  19462  fta1  19520  quotcan  19521  aalioulem4  19547  ulmcaulem  19603  ulmcn  19608  pilem2  19660  sincosq1lem  19697  sinq12gt0  19707  sinq12ge0  19708  sineq0  19721  tanord1  19731  lognegb  19775  logrec  19861  dcubic  19974  xrlimcnp  20095  o1cxp  20101  ftalem2  20143  ftalem3  20144  fsumdvdscom  20257  chtub  20283  vmasum  20287  bcmono  20348  bposlem3  20357  bposlem7  20361  lgsdir  20401  lgsqrlem2  20413  lgsdchr  20419  lgsquadlem2  20426  2sqlem6  20440  dchrisumlem3  20472  pntrsumbnd2  20548  pntpbnd1  20567  pntibnd  20574  pntlem3  20590  pntleml  20592  ex-natded5.3-2  20653  isgrpo  20693  opidon  20819  vacn  21097  ubthlem2  21280  htthlem  21327  normgt0  21536  shmodsi  21798  spansneleq  21979  h1datomi  21990  pjjsi  22127  nmcexi  22436  pjnormssi  22578  stm1add3i  22657  golem2  22682  cvnsym  22700  dmdmd  22710  mdslmd1lem1  22735  mdslmd1i  22739  mdexchi  22745  atcveq0  22758  superpos  22764  hatomistici  22772  atoml2i  22793  atcvat2i  22797  chirredlem1  22800  atcvat3i  22806  mdsymlem3  22815  mdsymlem5  22817  cdj3lem2b  22847  cdj3i  22851  subfacp1lem6  22887  iccllyscon  22952  cvmfolem  22981  cvmliftlem7  22993  cvmliftlem10  22996  eupath2  23075  ghomf1olem  23172  dedekind  23252  fundmpss  23290  dfon2lem3  23309  dfon2lem6  23312  axext4dist  23325  setlikess  23363  trpredtr  23401  trpredmintr  23402  dftrpred3g  23404  trpredrec  23409  frmin  23410  soseq  23422  wfrlem12  23435  frrlem5e  23457  frrlem11  23461  sltval2  23477  sltres  23485  axdenselem4  23506  axdenselem8  23510  axfelem6  23519  axfelem19  23532  dfrdg4  23662  brbtwn2  23707  colinearalg  23712  axcontlem10  23775  5segofs  23803  cgrextend  23805  segconeu  23808  btwncomim  23810  btwnswapid  23814  btwnintr  23816  btwnexch3  23817  btwndiff  23824  ifscgr  23841  cgrxfr  23852  btwnxfr  23853  lineext  23873  brofs2  23874  linecgr  23878  lineid  23880  idinside  23881  endofsegid  23882  btwnconn1lem13  23896  btwnconn3  23900  onsuct0  24054  limsucncmpi  24058  ubpar  24427  latdir  24461  intopcoaconc  24707  limfn3  24733  bwt2  24758  rdmob  24914  cmpmorp  24945  cmphmia  24964  cmphmib  24965  homgrf  24968  ismonc  24980  iepiclem  24989  isepic  24990  idfisf  25007  pgapspf2  25219  nbssntrs  25313  finminlem  25397  nn0prpwlem  25404  cldbnd  25410  clsint2  25413  reftr  25455  fnessref  25459  comppfsc  25473  neibastop3  25477  fgmin  25485  filbcmb  25598  nninfnub  25627  mettrifi  25639  geomcau  25641  istotbnd3  25661  sstotbnd2  25664  ismtybndlem  25696  heibor1lem  25699  heiborlem1  25701  heiborlem8  25708  heiborlem10  25710  heibor  25711  riscer  25785  crngohomfo  25797  keridl  25823  ispridl2  25829  ispridlc  25861  fphpdo  26066  icodiamlt  26071  pellexlem5  26084  pellexlem6  26085  jm2.26lem3  26260  dfac21  26330  unxpwdom3  26422  ordpss  26821  stoweidlem34  26917  19.41rg  27106  pwtrOLD  27386  ax10lem23X  27996  ax10lem24X  27997  ax10lem17ALT  28027  a12study10  28040  a12study10n  28041  ax9lem17  28060  lsatcveq0  28126  eqlkr3  28195  atlatmstc  28413  atlrelat1  28415  hlrelat2  28496  intnatN  28500  cvrexchlem  28512  cvratlem  28514  cvrat2  28522  atltcvr  28528  cvrat3  28535  cvrat4  28536  ps-1  28570  ps-2  28571  lplnnle2at  28634  lvolnle3at  28675  2llnma3r  28881  cdlemblem  28886  pmapjoin  28945  elpcliN  28986  lhpmcvr4N  29119  4atexlemnclw  29163  trlnidatb  29270  cdlemc4  29287  cdlemd3  29293  cdleme3g  29327  cdleme7d  29339  cdleme11c  29354  cdleme11dN  29355  cdleme21b  29419  cdleme21c  29420  cdleme21i  29428  cdleme22b  29434  cdleme35fnpq  29542  cdlemf1  29654  trlord  29662  cdlemg6c  29713  dihglblem6  30434  dochlkr  30479  dochkrshp  30480  dihjat1lem  30522  dochexmidlem5  30558  dochexmidlem8  30561
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator