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  1856  dral1-o  1857  cbv1h  1871  sbied  1909  sbequi  1952  ax11indalem  2114  ax11inda2ALT  2115  trel3  4095  poss  4288  sess2  4334  wefrc  4359  wereu2  4362  ordelord  4386  oninton  4563  orduniorsuc  4593  limuni3  4615  tfindsg  4623  limom  4643  funun  5234  ssimaex  5518  f1dmex  5685  f1imass  5722  soisoi  5759  isores3  5766  isofrlem  5771  isoselem  5772  weniso  5786  soxp  6162  riotasv3dOLD  6322  smoel  6345  smogt  6352  tfrlem9  6369  tz7.49  6425  seqomlem1  6430  abianfp  6439  odi  6545  omass  6546  omeulem2  6549  oeordsuc  6560  oeeulem  6567  ertr  6643  swoord2  6658  ecopovtrn  6729  domtriord  6975  2pwuninel  6984  onomeneq  7018  unxpdomlem2  7036  isinf  7044  pssnn  7049  findcard3  7068  frfi  7070  unblem3  7079  dffi3  7152  inf3lem3  7299  inf3lem5  7301  noinfep  7328  cantnfle  7340  cantnfp1lem3  7350  en3lplem1  7384  rankxpsuc  7520  tcrank  7522  ficardom  7562  carduni  7582  infxpenlem  7609  dfac8alem  7624  ac10ct  7629  ween  7630  alephdom  7676  alephle  7683  iscard3  7688  alephfp  7703  cdainf  7786  pwsdompw  7798  infdif  7803  cfslbn  7861  cofsmo  7863  cfsmolem  7864  cfcof  7868  fin1a2s  8008  domtriomlem  8036  ac6num  8074  zorn2lem3  8093  axdclem2  8115  imadomg  8127  iundom2g  8130  ficard  8155  fpwwe2lem8  8227  fpwwe2  8233  gchaclem  8260  tskr1om2  8358  inar1  8365  tskord  8370  tskuni  8373  grudomon  8407  grur1a  8409  grur1  8410  addnidpi  8493  ltexnq  8567  genpnnp  8597  addclprlem2  8609  mulclprlem  8611  psslinpr  8623  ltaddpr2  8627  ltexprlem6  8633  ltexprlem7  8634  addcanpr  8638  mulgt0sr  8695  map2psrpr  8700  supsrlem  8701  axrrecex  8753  letr  8882  recex  9368  lemul12b  9581  mulgt1  9583  ledivmulOLD  9598  fimaxre2  9670  lbreu  9672  nnrecgt0  9751  nnunb  9928  bndndx  9931  zeo  10064  uzind  10070  fzind  10076  fnn0ind  10077  lbzbi  10273  suprzcl2  10275  zmax  10280  rpnnen1lem5  10313  xrletr  10456  qbtwnre  10492  qsqueeze  10494  qextltlem  10495  xralrple  10498  xlesubadd  10549  supxrunb1  10604  icoshft  10724  fzen  10777  modadd1  10967  modmul1  10968  uzrdgfni  10987  seqcl2  11030  seqfveq2  11034  seqshft2  11038  monoord  11042  seqsplit  11045  seqf1olem1  11051  seqf1olem2  11052  seqid2  11058  seqhomo  11059  expnbnd  11196  faclbnd4lem4  11275  seqcoll  11366  sqeqd  11616  sqrmo  11702  cau3lem  11803  limsupbnd2  11922  lo1bdd2  11963  climuni  11991  rlimcn2  12029  mulcn2  12034  o1of2  12051  rlimo1  12055  lo1le  12090  isercolllem1  12103  iseralt  12122  isumrpcl  12264  cvgrat  12301  rpnnen2  12466  ruclem3  12473  sqr2irr  12489  dvds2lem  12503  dvdslelem  12535  divalglem8  12561  bitsinv1lem  12594  sadcaddlem  12610  smu01lem  12638  smueqlem  12643  bezoutlem4  12682  algcvga  12711  isprm3  12729  coprm  12741  coprmdvds2  12744  isprm5  12753  rpexp12i  12763  phibndlem  12800  dfphi2  12804  eulerthlem2  12812  odzdvds  12822  iserodd  12850  pclem  12853  pcpremul  12858  pcqcl  12871  pcdvdsb  12883  pcprmpw2  12896  pcaddlem  12898  pcmptcl  12901  pcfac  12909  prmpwdvds  12913  unbenlem  12917  prmreclem1  12925  4sqlem17  12970  vdwmc2  12988  vdwlem9  12998  vdwlem10  12999  vdwlem13  13002  vdwnnlem3  13006  ramcl  13038  mreiincl  13460  pospo  14069  dirge  14321  oddvdsnn0  14821  oddvds  14824  odcl2  14840  gexdvds  14857  sylow1lem1  14871  sylow2alem2  14891  sylow2a  14892  efgi2  14996  efgsrel  15005  efgs1b  15007  cyggex2  15145  pgpfac1lem2  15272  pgpfac1lem3a  15273  pgpfac1lem3  15274  pgpfac1lem5  15276  lssssr  15672  gzrngunitlem  16398  znunit  16479  frgpcyg  16489  lsmcss  16554  obselocv  16590  obslbs  16592  ordtrest2lem  16895  leordtval2  16904  lecldbas  16911  cncls  16965  cncnp  16971  cnpresti  16978  lmcnp  16994  cnt0  17036  isreg2  17067  cmpsublem  17088  cmpsub  17089  tgcmp  17090  dfcon2  17107  1stcfb  17133  2ndcctbss  17143  1stcelcls  17149  islly2  17172  dislly  17185  kgencn2  17214  txcnp  17276  txindis  17290  txcmplem1  17297  txlm  17304  xkohaus  17309  cnmptcom  17334  kqfvima  17383  isr0  17390  fgss2  17531  fbasrn  17541  filuni  17542  ufilmax  17564  isufil2  17565  cfinufil  17585  fmfnfmlem1  17611  fmfnfmlem2  17612  fmfnfmlem4  17614  fmfnfm  17615  fmco  17618  flimopn  17632  hausflim  17638  flimrest  17640  fclsopn  17671  flimfnfcls  17685  alexsubALTlem2  17704  alexsubALTlem3  17705  alexsubALT  17707  ptcmplem2  17709  symgtgp  17746  divstgplem  17765  tsmsres  17788  tsmsxplem1  17797  imasdsf1olem  17899  bldisj  17917  blss  17934  metcnp3  18048  ngptgp  18114  nrginvrcn  18164  nmoleub  18202  xrsmopn  18280  icccmplem3  18291  reconnlem2  18294  rectbntr0  18299  rescncf  18363  icoopnst  18399  iocopnst  18400  iccpnfcnv  18404  lebnumii  18426  nmoleub2lem  18557  nmhmcn  18563  fgcfil  18659  iscfil3  18661  iscau2  18665  iscau3  18666  iscau4  18667  iscmet3lem2  18680  cfilres  18684  caussi  18685  equivcfil  18687  equivcau  18688  caubl  18695  ivthlem2  18774  ivthlem3  18775  ovoliunlem2  18824  ovoliunnul  18828  ovolicc2lem3  18840  ioombl1lem4  18880  dyadmax  18915  dyadmbl  18917  volsup2  18922  itg2le  19056  itg2const2  19058  itg2seq  19059  itgsplitioo  19154  dvnres  19242  rolle  19299  c1lip1  19306  dvivthlem1  19317  lhop1  19323  dvcnvrelem1  19326  dvfsumrlim  19340  ply1divmo  19483  ig1peu  19519  plypf1  19556  coeaddlem  19592  fta1  19650  quotcan  19651  aalioulem4  19677  ulmcaulem  19733  ulmcn  19738  pilem2  19790  sincosq1lem  19827  sinq12gt0  19837  sinq12ge0  19838  sineq0  19851  tanord1  19861  lognegb  19905  logrec  20079  dcubic  20104  xrlimcnp  20225  o1cxp  20231  ftalem2  20273  ftalem3  20274  fsumdvdscom  20387  chtub  20413  vmasum  20417  bcmono  20478  bposlem3  20487  bposlem7  20491  lgsdir  20531  lgsqrlem2  20543  lgsdchr  20549  lgsquadlem2  20556  2sqlem6  20570  dchrisumlem3  20602  pntrsumbnd2  20678  pntpbnd1  20697  pntibnd  20704  pntlem3  20720  pntleml  20722  ex-natded5.3-2  20783  isgrpo  20823  opidon  20949  vacn  21227  ubthlem2  21410  htthlem  21457  normgt0  21666  shmodsi  21928  spansneleq  22109  h1datomi  22120  pjjsi  22239  nmcexi  22566  pjnormssi  22708  stm1add3i  22787  golem2  22812  cvnsym  22830  dmdmd  22840  mdslmd1lem1  22865  mdslmd1i  22869  mdexchi  22875  atcveq0  22888  superpos  22894  hatomistici  22902  atoml2i  22923  atcvat2i  22927  chirredlem1  22930  atcvat3i  22936  mdsymlem3  22945  mdsymlem5  22947  cdj3lem2b  22977  cdj3i  22981  ifeqeqx  22994  ballotlemfc0  23012  ballotlemfcc  23013  ballotlemfrceq  23048  subfacp1lem6  23088  iccllyscon  23153  cvmfolem  23182  cvmliftlem7  23194  cvmliftlem10  23197  eupath2  23276  ghomf1olem  23373  dedekind  23453  fundmpss  23491  dfon2lem3  23510  dfon2lem6  23513  axext4dist  23526  setlikess  23564  trpredtr  23602  trpredmintr  23603  dftrpred3g  23605  trpredrec  23610  frmin  23611  soseq  23623  wfrlem12  23636  frrlem5e  23658  frrlem11  23662  sltval2  23678  sltres  23686  axdenselem4  23707  axdenselem8  23711  axfelem6  23720  axfelem19  23733  dfrdg4  23863  brbtwn2  23908  colinearalg  23913  axcontlem10  23976  5segofs  24004  cgrextend  24006  segconeu  24009  btwncomim  24011  btwnswapid  24015  btwnintr  24017  btwnexch3  24018  btwndiff  24025  ifscgr  24042  cgrxfr  24053  btwnxfr  24054  lineext  24074  brofs2  24075  linecgr  24079  lineid  24081  idinside  24082  endofsegid  24083  btwnconn1lem13  24097  btwnconn3  24101  onsuct0  24255  limsucncmpi  24259  ubpar  24628  latdir  24662  intopcoaconc  24908  limfn3  24934  bwt2  24959  rdmob  25115  cmpmorp  25146  cmphmia  25165  cmphmib  25166  homgrf  25169  ismonc  25181  iepiclem  25190  isepic  25191  idfisf  25208  pgapspf2  25420  nbssntrs  25514  finminlem  25598  nn0prpwlem  25605  cldbnd  25611  clsint2  25614  reftr  25656  fnessref  25660  comppfsc  25674  neibastop3  25678  fgmin  25686  filbcmb  25799  nninfnub  25828  mettrifi  25840  geomcau  25842  istotbnd3  25862  sstotbnd2  25865  ismtybndlem  25897  heibor1lem  25900  heiborlem1  25902  heiborlem8  25909  heiborlem10  25911  heibor  25912  riscer  25986  crngohomfo  25998  keridl  26024  ispridl2  26030  ispridlc  26062  fphpdo  26267  icodiamlt  26272  pellexlem5  26285  pellexlem6  26286  jm2.26lem3  26461  dfac21  26531  unxpwdom3  26623  ordpss  27022  stoweidlem34  27118  19.41rg  27369  pwtrOLD  27649  ax10lem23X  28259  ax10lem24X  28260  ax10lem17ALT  28290  a12study10  28303  a12study10n  28304  ax9lem17  28323  lsatcveq0  28389  eqlkr3  28458  atlatmstc  28676  atlrelat1  28678  hlrelat2  28759  intnatN  28763  cvrexchlem  28775  cvratlem  28777  cvrat2  28785  atltcvr  28791  cvrat3  28798  cvrat4  28799  ps-1  28833  ps-2  28834  lplnnle2at  28897  lvolnle3at  28938  2llnma3r  29144  cdlemblem  29149  pmapjoin  29208  elpcliN  29249  lhpmcvr4N  29382  4atexlemnclw  29426  trlnidatb  29533  cdlemc4  29550  cdlemd3  29556  cdleme3g  29590  cdleme7d  29602  cdleme11c  29617  cdleme11dN  29618  cdleme21b  29682  cdleme21c  29683  cdleme21i  29691  cdleme22b  29697  cdleme35fnpq  29805  cdlemf1  29917  trlord  29925  cdlemg6c  29976  dihglblem6  30697  dochlkr  30742  dochkrshp  30743  dihjat1lem  30785  dochexmidlem5  30821  dochexmidlem8  30824
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator