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

Theorem syld 40
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 40 has the same form as syl 15 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 19 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 22 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpdd 36 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  3syld  51  sylsyld  52  nsyld  132  pm2.61d  150  sylibd  205  sylbid  206  sylibrd  225  sylbird  226  syland  467  alrimdd  1769  dvelimv  1944  ax10lem6  1948  dral1  1970  cbv1h  1983  sbied  2041  sbequi  2064  dral1-o  2159  ax11indalem  2202  ax11inda2ALT  2203  trel3  4200  poss  4395  sess2  4441  wefrc  4466  wereu2  4469  ordelord  4493  oninton  4670  orduniorsuc  4700  limuni3  4722  tfindsg  4730  limom  4750  funun  5375  ssimaex  5664  f1dmex  5834  f1imass  5872  soisoi  5909  isores3  5916  isofrlem  5921  isoselem  5922  weniso  5936  soxp  6312  riotasv3dOLD  6438  smoel  6461  smogt  6468  tfrlem9  6485  tz7.49  6541  seqomlem1  6546  abianfp  6555  odi  6661  omass  6662  omeulem2  6665  oeordsuc  6676  oeeulem  6683  ertr  6759  swoord2  6774  ecopovtrn  6846  domtriord  7092  2pwuninel  7101  onomeneq  7135  unxpdomlem2  7153  isinf  7161  pssnn  7166  findcard3  7187  frfi  7189  unblem3  7198  dffi3  7271  inf3lem3  7418  inf3lem5  7420  noinfep  7447  cantnfle  7459  cantnfp1lem3  7469  en3lplem1  7503  rankxpsuc  7639  tcrank  7641  ficardom  7681  carduni  7701  infxpenlem  7728  dfac8alem  7743  ac10ct  7748  ween  7749  alephdom  7795  alephle  7802  iscard3  7807  alephfp  7822  cdainf  7905  pwsdompw  7917  infdif  7922  cfslbn  7980  cofsmo  7982  cfsmolem  7983  cfcof  7987  fin1a2s  8127  domtriomlem  8155  ac6num  8193  zorn2lem3  8212  axdclem2  8234  imadomg  8246  iundom2g  8249  ficard  8274  fpwwe2lem8  8346  fpwwe2  8352  gchaclem  8379  tskr1om2  8477  inar1  8484  tskord  8489  tskuni  8492  grudomon  8526  grur1a  8528  grur1  8529  addnidpi  8612  ltexnq  8686  genpnnp  8716  addclprlem2  8728  mulclprlem  8730  psslinpr  8742  ltaddpr2  8746  ltexprlem6  8752  ltexprlem7  8753  addcanpr  8757  mulgt0sr  8814  map2psrpr  8819  supsrlem  8820  axrrecex  8872  letr  9001  recex  9487  lemul12b  9700  mulgt1  9702  ledivmulOLD  9717  fimaxre2  9789  lbreu  9791  nnrecgt0  9870  nnunb  10050  bndndx  10053  zeo  10186  uzind  10192  fzind  10199  fnn0ind  10200  lbzbi  10395  suprzcl2  10397  zmax  10402  rpnnen1lem5  10435  xrletr  10578  qbtwnre  10615  qsqueeze  10617  qextltlem  10618  xralrple  10621  xlesubadd  10672  supxrunb1  10727  icoshft  10847  fzen  10900  modadd1  11090  modmul1  11091  uzrdgfni  11110  seqcl2  11153  seqfveq2  11157  seqshft2  11161  monoord  11165  seqsplit  11168  seqf1olem1  11174  seqf1olem2  11175  seqid2  11181  seqhomo  11182  expnbnd  11320  faclbnd4lem4  11399  seqcoll  11491  sqeqd  11741  sqrmo  11827  cau3lem  11928  limsupbnd2  12047  lo1bdd2  12088  climuni  12116  rlimcn2  12154  mulcn2  12159  o1of2  12176  rlimo1  12180  lo1le  12215  isercolllem1  12228  iseralt  12248  isumrpcl  12393  cvgrat  12430  rpnnen2  12595  ruclem3  12602  sqr2irr  12618  dvds2lem  12632  dvdslelem  12664  divalglem8  12690  bitsinv1lem  12723  sadcaddlem  12739  smu01lem  12767  smueqlem  12772  bezoutlem4  12811  algcvga  12840  isprm3  12858  coprm  12870  coprmdvds2  12873  isprm5  12882  rpexp12i  12892  phibndlem  12929  dfphi2  12933  eulerthlem2  12941  odzdvds  12951  iserodd  12979  pclem  12982  pcpremul  12987  pcqcl  13000  pcdvdsb  13012  pcprmpw2  13025  pcaddlem  13027  pcmptcl  13030  pcfac  13038  prmpwdvds  13042  unbenlem  13046  prmreclem1  13054  4sqlem17  13099  vdwmc2  13117  vdwlem9  13127  vdwlem10  13128  vdwlem13  13131  vdwnnlem3  13135  ramcl  13167  mreiincl  13591  pospo  14200  dirge  14452  oddvdsnn0  14952  oddvds  14955  odcl2  14971  gexdvds  14988  sylow1lem1  15002  sylow2alem2  15022  sylow2a  15023  efgi2  15127  efgsrel  15136  efgs1b  15138  cyggex2  15276  pgpfac1lem2  15403  pgpfac1lem3a  15404  pgpfac1lem3  15405  pgpfac1lem5  15407  lssssr  15803  gzrngunitlem  16536  znunit  16617  frgpcyg  16627  lsmcss  16692  obselocv  16728  obslbs  16730  ordtrest2lem  17033  leordtval2  17042  lecldbas  17049  cncls  17103  cncnp  17109  cnpresti  17116  lmcnp  17132  cnt0  17174  isreg2  17205  cmpsublem  17226  cmpsub  17227  tgcmp  17228  dfcon2  17245  1stcfb  17271  2ndcctbss  17281  1stcelcls  17287  islly2  17310  dislly  17323  kgencn2  17352  txcnp  17414  txindis  17428  txcmplem1  17435  txlm  17442  xkohaus  17447  cnmptcom  17472  kqfvima  17521  isr0  17528  fgss2  17665  fbasrn  17675  filuni  17676  ufilmax  17698  isufil2  17699  cfinufil  17719  fmfnfmlem1  17745  fmfnfmlem2  17746  fmfnfmlem4  17748  fmfnfm  17749  fmco  17752  flimopn  17766  hausflim  17772  flimrest  17774  fclsopn  17805  flimfnfcls  17819  alexsubALTlem2  17838  alexsubALTlem3  17839  alexsubALT  17841  ptcmplem2  17843  symgtgp  17880  divstgplem  17899  tsmsres  17922  tsmsxplem1  17931  imasdsf1olem  18033  bldisj  18051  blss  18068  metcnp3  18182  ngptgp  18248  nrginvrcn  18298  nmoleub  18336  xrsmopn  18414  icccmplem3  18426  reconnlem2  18429  rectbntr0  18434  rescncf  18498  icoopnst  18535  iocopnst  18536  iccpnfcnv  18540  lebnumii  18562  nmoleub2lem  18693  nmhmcn  18699  fgcfil  18795  iscfil3  18797  iscau2  18801  iscau3  18802  iscau4  18803  iscmet3lem2  18816  cfilres  18820  caussi  18821  equivcfil  18823  equivcau  18824  caubl  18831  ivthlem2  18910  ivthlem3  18911  ovoliunlem2  18960  ovoliunnul  18964  ovolicc2lem3  18976  ioombl1lem4  19016  dyadmax  19051  dyadmbl  19053  volsup2  19058  itg2le  19192  itg2const2  19194  itg2seq  19195  itgsplitioo  19290  dvnres  19378  rolle  19435  c1lip1  19442  dvivthlem1  19453  lhop1  19459  dvcnvrelem1  19462  dvfsumrlim  19476  ply1divmo  19619  ig1peu  19655  plypf1  19692  coeaddlem  19728  fta1  19786  quotcan  19787  aalioulem4  19813  ulmcaulem  19871  ulmcn  19876  pilem2  19929  sincosq1lem  19966  sinq12gt0  19976  sinq12ge0  19977  sineq0  19990  tanord1  20000  lognegb  20045  logrec  20222  dcubic  20247  xrlimcnp  20368  o1cxp  20374  ftalem2  20417  ftalem3  20418  fsumdvdscom  20531  chtub  20557  vmasum  20561  bcmono  20622  bposlem3  20631  bposlem7  20635  lgsdir  20675  lgsqrlem2  20687  lgsdchr  20693  lgsquadlem2  20700  2sqlem6  20714  dchrisumlem3  20746  pntrsumbnd2  20822  pntpbnd1  20841  pntibnd  20848  pntlem3  20864  pntleml  20866  ex-natded5.3-2  20901  isgrpo  20969  opidon  21095  vacn  21375  ubthlem2  21558  htthlem  21605  normgt0  21814  shmodsi  22076  spansneleq  22257  h1datomi  22268  pjjsi  22387  nmcexi  22714  pjnormssi  22856  stm1add3i  22935  golem2  22960  cvnsym  22978  dmdmd  22988  mdslmd1lem1  23013  mdslmd1i  23017  mdexchi  23023  atcveq0  23036  superpos  23042  hatomistici  23050  atoml2i  23071  atcvat2i  23075  chirredlem1  23078  atcvat3i  23084  mdsymlem3  23093  mdsymlem5  23095  cdj3lem2b  23125  cdj3i  23129  bisimpd  23135  ifeqeqx  23197  supssd  23299  cnre2csqlem  23464  tpr2rico  23466  xrge0iifcnv  23475  cnextcn  23504  sigaclci  23781  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemfrceq  24035  subfacp1lem6  24120  iccllyscon  24185  cvmfolem  24214  cvmliftlem7  24226  cvmliftlem10  24229  eupath2  24308  ghomf1olem  24405  dedekind  24488  fprodss  24575  fundmpss  24680  dfon2lem3  24699  dfon2lem6  24702  axext4dist  24715  setlikess  24753  trpredtr  24791  trpredmintr  24792  dftrpred3g  24794  trpredrec  24799  frmin  24800  soseq  24812  wfrlem12  24825  frrlem5e  24847  frrlem11  24851  sltval2  24868  sltres  24876  nodenselem4  24896  nodenselem8  24900  nobndlem6  24909  dfrdg4  25047  brbtwn2  25092  colinearalg  25097  axcontlem10  25160  5segofs  25188  cgrextend  25190  segconeu  25193  btwncomim  25195  btwnswapid  25199  btwnintr  25201  btwnexch3  25202  btwndiff  25209  ifscgr  25226  cgrxfr  25237  btwnxfr  25238  lineext  25258  brofs2  25259  linecgr  25263  lineid  25265  idinside  25266  endofsegid  25267  btwnconn1lem13  25281  btwnconn3  25285  onsuct0  25439  limsucncmpi  25443  ltflcei  25485  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  itg2gt0cn  25495  finminlem  25555  nn0prpwlem  25562  cldbnd  25568  clsint2  25571  reftr  25613  fnessref  25617  comppfsc  25631  neibastop3  25635  fgmin  25643  filbcmb  25756  nninfnub  25785  mettrifi  25797  geomcau  25799  istotbnd3  25818  sstotbnd2  25821  ismtybndlem  25853  heibor1lem  25856  heiborlem1  25858  heiborlem8  25865  heiborlem10  25867  heibor  25868  riscer  25942  crngohomfo  25954  keridl  25980  ispridl2  25986  ispridlc  26018  fphpdo  26223  icodiamlt  26228  pellexlem5  26241  pellexlem6  26242  jm2.26lem3  26417  dfac21  26487  unxpwdom3  26579  ordpss  26977  stoweidlem34  27106  redwlk  27725  fargshiftf1  27743  constr3trllem2  27758  4cycl4dv  27774  vdusgra0nedg  27799  usgravd0nedg  27803  19.41rg  28044  pwtrOLD  28344  dvelimvNEW7  28868  dral1NEW7  28899  cbv1hwAUX7  28917  sbiedNEW7  28944  sbequiNEW7  28982  hbaew4AUX7  29048  cbv1hOLD7  29103  ax10lem17ALT  29175  a12study10  29188  a12study10n  29189  ax9lem17  29208  lsatcveq0  29274  eqlkr3  29343  atlatmstc  29561  atlrelat1  29563  hlrelat2  29644  intnatN  29648  cvrexchlem  29660  cvratlem  29662  cvrat2  29670  atltcvr  29676  cvrat3  29683  cvrat4  29684  ps-1  29718  ps-2  29719  lplnnle2at  29782  lvolnle3at  29823  2llnma3r  30029  cdlemblem  30034  pmapjoin  30093  elpcliN  30134  lhpmcvr4N  30267  4atexlemnclw  30311  trlnidatb  30418  cdlemc4  30435  cdlemd3  30441  cdleme3g  30475  cdleme7d  30487  cdleme11c  30502  cdleme11dN  30503  cdleme21b  30567  cdleme21c  30568  cdleme21i  30576  cdleme22b  30582  cdleme35fnpq  30690  cdlemf1  30802  trlord  30810  cdlemg6c  30861  dihglblem6  31582  dochlkr  31627  dochkrshp  31628  dihjat1lem  31670  dochexmidlem5  31706  dochexmidlem8  31709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator