MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld Structured version   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 16 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 20 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 23 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpdd 38 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  3syld  53  sylsyld  54  nsyld  134  pm2.61d  152  sylibd  206  sylbid  207  sylibrd  226  sylbird  227  syland  468  alrimdd  1784  cbv1hOLD  1975  ax12olem3  2007  ax10o2  2024  dvelimvOLD  2028  dral1OLD  2058  sbequi  2110  sbequiOLD  2114  sbiedOLD  2151  dral1-o  2231  ax11indalem  2274  ax11inda2ALT  2275  trel3  4310  poss  4505  sess2  4551  wefrc  4576  wereu2  4579  ordelord  4603  oninton  4780  orduniorsuc  4810  limuni3  4832  tfindsg  4840  limom  4860  funun  5495  ssimaex  5788  f1dmex  5971  f1imass  6010  soisoi  6048  isores3  6055  isofrlem  6060  isoselem  6061  weniso  6075  f1o2ndf1  6454  soxp  6459  riotasv3dOLD  6599  smoel  6622  smogt  6629  tfrlem9  6646  tz7.49  6702  seqomlem1  6707  abianfp  6716  odi  6822  omass  6823  omeulem2  6826  oeordsuc  6837  oeeulem  6844  ertr  6920  swoord2  6935  ecopovtrn  7007  domtriord  7253  2pwuninel  7262  onomeneq  7296  unxpdomlem2  7314  isinf  7322  pssnn  7327  findcard3  7350  frfi  7352  unblem3  7361  dffi3  7436  inf3lem3  7585  inf3lem5  7587  noinfep  7614  cantnfle  7626  cantnfp1lem3  7636  en3lplem1  7670  rankxpsuc  7806  tcrank  7808  ficardom  7848  carduni  7868  infxpenlem  7895  dfac8alem  7910  ac10ct  7915  ween  7916  alephdom  7962  alephle  7969  iscard3  7974  alephfp  7989  cdainf  8072  pwsdompw  8084  infdif  8089  cfslbn  8147  cofsmo  8149  cfsmolem  8150  cfcof  8154  fin1a2s  8294  domtriomlem  8322  ac6num  8359  zorn2lem3  8378  axdclem2  8400  imadomg  8412  iundom2g  8415  ficard  8440  fpwwe2lem8  8512  fpwwe2  8518  gchaclem  8545  tskr1om2  8643  inar1  8650  tskord  8655  tskuni  8658  grudomon  8692  grur1a  8694  grur1  8695  addnidpi  8778  ltexnq  8852  genpnnp  8882  addclprlem2  8894  mulclprlem  8896  psslinpr  8908  ltaddpr2  8912  ltexprlem6  8918  ltexprlem7  8919  addcanpr  8923  mulgt0sr  8980  map2psrpr  8985  supsrlem  8986  axrrecex  9038  letr  9167  recex  9654  lemul12b  9867  mulgt1  9869  ledivmulOLD  9884  fimaxre2  9956  lbreu  9958  nnrecgt0  10037  nnunb  10217  bndndx  10220  zeo  10355  uzind  10361  fzind  10368  fnn0ind  10369  lbzbi  10564  suprzcl2  10566  zmax  10571  rpnnen1lem5  10604  xrletr  10748  qbtwnre  10785  qsqueeze  10787  qextltlem  10788  xralrple  10791  xlesubadd  10842  supxrunb1  10898  icoshft  11019  fzen  11072  modadd1  11278  modmul1  11279  uzrdgfni  11298  seqcl2  11341  seqfveq2  11345  seqshft2  11349  monoord  11353  seqsplit  11356  seqf1olem1  11362  seqf1olem2  11363  seqid2  11369  seqhomo  11370  expnbnd  11508  faclbnd4lem4  11587  seqcoll  11712  sqeqd  11971  sqrmo  12057  cau3lem  12158  limsupbnd2  12277  lo1bdd2  12318  climuni  12346  rlimcn2  12384  mulcn2  12389  o1of2  12406  rlimo1  12410  lo1le  12445  isercolllem1  12458  iseralt  12478  isumrpcl  12623  cvgrat  12660  rpnnen2  12825  ruclem3  12832  sqr2irr  12848  dvds2lem  12862  dvdslelem  12894  divalglem8  12920  bitsinv1lem  12953  sadcaddlem  12969  smu01lem  12997  smueqlem  13002  bezoutlem4  13041  algcvga  13070  isprm3  13088  coprm  13100  coprmdvds2  13103  isprm5  13112  rpexp12i  13122  phibndlem  13159  dfphi2  13163  eulerthlem2  13171  odzdvds  13181  iserodd  13209  pclem  13212  pcpremul  13217  pcqcl  13230  pcdvdsb  13242  pcprmpw2  13255  pcaddlem  13257  pcmptcl  13260  pcfac  13268  prmpwdvds  13272  unbenlem  13276  prmreclem1  13284  4sqlem17  13329  vdwmc2  13347  vdwlem9  13357  vdwlem10  13358  vdwlem13  13361  vdwnnlem3  13365  ramcl  13397  mreiincl  13821  pospo  14430  dirge  14682  oddvdsnn0  15182  oddvds  15185  odcl2  15201  gexdvds  15218  sylow1lem1  15232  sylow2alem2  15252  sylow2a  15253  efgi2  15357  efgsrel  15366  efgs1b  15368  cyggex2  15506  pgpfac1lem2  15633  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfac1lem5  15637  lssssr  16029  gzrngunitlem  16763  znunit  16844  frgpcyg  16854  lsmcss  16919  obselocv  16955  obslbs  16957  ordtrest2lem  17267  leordtval2  17276  lecldbas  17283  cncls  17338  cncnp  17344  cnpresti  17352  lmcnp  17368  cnt0  17410  isreg2  17441  cmpsublem  17462  cmpsub  17463  tgcmp  17464  bwth  17473  dfcon2  17482  1stcfb  17508  2ndcctbss  17518  1stcelcls  17524  islly2  17547  dislly  17560  kgencn2  17589  txcnp  17652  txindis  17666  txcmplem1  17673  txlm  17680  xkohaus  17685  cnmptcom  17710  kqfvima  17762  isr0  17769  fgss2  17906  fbasrn  17916  filuni  17917  ufilmax  17939  isufil2  17940  cfinufil  17960  fmfnfmlem1  17986  fmfnfmlem2  17987  fmfnfmlem4  17989  fmfnfm  17990  fmco  17993  flimopn  18007  hausflim  18013  flimrest  18015  fclsopn  18046  flimfnfcls  18060  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALT  18082  ptcmplem2  18084  cnextcn  18098  symgtgp  18131  divstgplem  18150  tsmsres  18173  tsmsxplem1  18182  isucn2  18309  imasdsf1olem  18403  bldisj  18428  blssps  18454  blss  18455  metcnp3  18570  ngptgp  18677  nrginvrcn  18727  nmoleub  18765  xrsmopn  18843  icccmplem3  18855  reconnlem2  18858  rectbntr0  18863  rescncf  18927  icoopnst  18964  iocopnst  18965  iccpnfcnv  18969  lebnumii  18991  nmoleub2lem  19122  nmhmcn  19128  fgcfil  19224  iscfil3  19226  iscau2  19230  iscau3  19231  iscau4  19232  iscmet3lem2  19245  cfilres  19249  caussi  19250  equivcfil  19252  equivcau  19253  caubl  19260  ivthlem2  19349  ivthlem3  19350  ovoliunlem2  19399  ovoliunnul  19403  ovolicc2lem3  19415  ioombl1lem4  19455  dyadmax  19490  dyadmbl  19492  volsup2  19497  itg2le  19631  itg2const2  19633  itg2seq  19634  itgsplitioo  19729  dvnres  19817  rolle  19874  c1lip1  19881  dvivthlem1  19892  lhop1  19898  dvcnvrelem1  19901  dvfsumrlim  19915  ply1divmo  20058  ig1peu  20094  plypf1  20131  coeaddlem  20167  fta1  20225  quotcan  20226  aalioulem4  20252  ulmcaulem  20310  ulmcn  20315  pilem2  20368  sincosq1lem  20405  sinq12gt0  20415  sinq12ge0  20416  sineq0  20429  tanord1  20439  lognegb  20484  logrec  20661  dcubic  20686  xrlimcnp  20807  o1cxp  20813  ftalem2  20856  ftalem3  20857  fsumdvdscom  20970  chtub  20996  vmasum  21000  bcmono  21061  bposlem3  21070  bposlem7  21074  lgsdir  21114  lgsqrlem2  21126  lgsdchr  21132  lgsquadlem2  21139  2sqlem6  21153  dchrisumlem3  21185  pntrsumbnd2  21261  pntpbnd1  21280  pntibnd  21287  pntlem3  21303  pntleml  21305  redwlk  21606  fargshiftf1  21624  constr3trllem2  21638  4cycl4dv  21654  vdusgra0nedg  21679  usgravd0nedg  21683  eupath2  21702  isgrpo  21784  opidon  21910  vacn  22190  ubthlem2  22373  htthlem  22420  normgt0  22629  shmodsi  22891  spansneleq  23072  h1datomi  23083  pjjsi  23202  nmcexi  23529  pjnormssi  23671  stm1add3i  23750  golem2  23775  cvnsym  23793  dmdmd  23803  mdslmd1lem1  23828  mdslmd1i  23832  mdexchi  23838  atcveq0  23851  superpos  23857  hatomistici  23865  atoml2i  23886  atcvat2i  23890  chirredlem1  23893  atcvat3i  23899  mdsymlem3  23908  mdsymlem5  23910  cdj3lem2b  23940  cdj3i  23944  supssd  24098  resspos  24187  resstos  24188  tpr2rico  24310  xrge0iifcnv  24319  ballotlemfc0  24750  ballotlemfcc  24751  subfacp1lem6  24871  iccllyscon  24937  cvmfolem  24966  cvmliftlem7  24978  cvmliftlem10  24981  ghomf1olem  25105  dedekind  25187  fprodss  25274  fundmpss  25390  dfon2lem3  25412  dfon2lem6  25415  axext4dist  25428  setlikess  25470  trpredtr  25508  trpredmintr  25509  dftrpred3g  25511  trpredrec  25516  frmin  25517  soseq  25529  wfrlem12  25549  frrlem5e  25590  frrlem11  25594  sltval2  25611  sltres  25619  nodenselem4  25639  nodenselem8  25643  nobndlem6  25652  dfrdg4  25795  brbtwn2  25844  colinearalg  25849  axcontlem10  25912  5segofs  25940  cgrextend  25942  segconeu  25945  btwncomim  25947  btwnswapid  25951  btwnintr  25953  btwnexch3  25954  btwndiff  25961  ifscgr  25978  cgrxfr  25989  btwnxfr  25990  lineext  26010  brofs2  26011  linecgr  26015  lineid  26017  idinside  26018  endofsegid  26019  btwnconn1lem13  26033  btwnconn3  26037  onsuct0  26191  limsucncmpi  26195  ltflcei  26239  mblfinlem2  26244  mblfinlem3  26245  itg2addnclem  26256  itg2addnclem2  26257  itg2gt0cn  26260  ftc1anclem5  26284  ftc1anclem6  26285  finminlem  26321  nn0prpwlem  26325  cldbnd  26329  clsint2  26332  reftr  26369  fnessref  26373  comppfsc  26387  neibastop3  26391  fgmin  26399  filbcmb  26442  nninfnub  26455  mettrifi  26463  geomcau  26465  istotbnd3  26480  sstotbnd2  26483  ismtybndlem  26515  heibor1lem  26518  heiborlem1  26520  heiborlem8  26527  heiborlem10  26529  heibor  26530  riscer  26604  crngohomfo  26616  keridl  26642  ispridl2  26648  ispridlc  26680  fphpdo  26878  icodiamlt  26883  pellexlem5  26896  pellexlem6  26897  jm2.26lem3  27072  dfac21  27141  unxpwdom3  27233  ordpss  27630  stoweidlem34  27759  ltsubnn0  28097  elfz2z  28105  elfzmlbm  28106  elfzmlbp  28107  elfz0fzfz0  28114  ubmelm1fzo  28127  fzo1fzo0n0  28128  fzofzim  28136  wrdlenge2n0  28176  swrdnd  28182  swrdvalodmlem1  28187  swrdvalodm2  28188  swrdswrdlem  28198  swrdswrd  28199  swrdccatin12lem3a  28208  swrdccatin12lem3b  28209  swrdccatin12lem4  28213  swrdccat3a  28217  swrdccat3blem  28218  2cshw1lem1  28248  2cshw1lem2  28249  2cshwmod  28257  cshweqdif2s  28271  usg2wlkeq  28304  usgra2adedgspthlem2  28314  usg2wotspth  28351  19.41rg  28637  dvelimvNEW7  29462  dral1NEW7  29493  cbv1hwAUX7  29511  sbiedNEW7  29540  sbequiNEW7  29579  ax7w15lemxAUX7  29666  cbv1hOLD7  29719  lsatcveq0  29830  eqlkr3  29899  atlatmstc  30117  atlrelat1  30119  hlrelat2  30200  intnatN  30204  cvrexchlem  30216  cvratlem  30218  cvrat2  30226  atltcvr  30232  cvrat3  30239  cvrat4  30240  ps-1  30274  ps-2  30275  lplnnle2at  30338  lvolnle3at  30379  2llnma3r  30585  cdlemblem  30590  pmapjoin  30649  elpcliN  30690  lhpmcvr4N  30823  4atexlemnclw  30867  trlnidatb  30974  cdlemc4  30991  cdlemd3  30997  cdleme3g  31031  cdleme7d  31043  cdleme11c  31058  cdleme11dN  31059  cdleme21b  31123  cdleme21c  31124  cdleme21i  31132  cdleme22b  31138  cdleme35fnpq  31246  cdlemf1  31358  trlord  31366  cdlemg6c  31417  dihglblem6  32138  dochlkr  32183  dochkrshp  32184  dihjat1lem  32226  dochexmidlem5  32262  dochexmidlem8  32265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator