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  alrimdd  1750  dvelimv  1881  ax10lem6  1885  dral1  1908  cbv1h  1921  sbied  1982  sbequi  1999  dral1-o  2096  ax11indalem  2138  ax11inda2ALT  2139  trel3  4123  poss  4316  sess2  4362  wefrc  4387  wereu2  4390  ordelord  4414  oninton  4591  orduniorsuc  4621  limuni3  4643  tfindsg  4651  limom  4671  funun  5262  ssimaex  5546  f1dmex  5713  f1imass  5750  soisoi  5787  isores3  5794  isofrlem  5799  isoselem  5800  weniso  5814  soxp  6190  riotasv3dOLD  6350  smoel  6373  smogt  6380  tfrlem9  6397  tz7.49  6453  seqomlem1  6458  abianfp  6467  odi  6573  omass  6574  omeulem2  6577  oeordsuc  6588  oeeulem  6595  ertr  6671  swoord2  6686  ecopovtrn  6757  domtriord  7003  2pwuninel  7012  onomeneq  7046  unxpdomlem2  7064  isinf  7072  pssnn  7077  findcard3  7096  frfi  7098  unblem3  7107  dffi3  7180  inf3lem3  7327  inf3lem5  7329  noinfep  7356  cantnfle  7368  cantnfp1lem3  7378  en3lplem1  7412  rankxpsuc  7548  tcrank  7550  ficardom  7590  carduni  7610  infxpenlem  7637  dfac8alem  7652  ac10ct  7657  ween  7658  alephdom  7704  alephle  7711  iscard3  7716  alephfp  7731  cdainf  7814  pwsdompw  7826  infdif  7831  cfslbn  7889  cofsmo  7891  cfsmolem  7892  cfcof  7896  fin1a2s  8036  domtriomlem  8064  ac6num  8102  zorn2lem3  8121  axdclem2  8143  imadomg  8155  iundom2g  8158  ficard  8183  fpwwe2lem8  8255  fpwwe2  8261  gchaclem  8288  tskr1om2  8386  inar1  8393  tskord  8398  tskuni  8401  grudomon  8435  grur1a  8437  grur1  8438  addnidpi  8521  ltexnq  8595  genpnnp  8625  addclprlem2  8637  mulclprlem  8639  psslinpr  8651  ltaddpr2  8655  ltexprlem6  8661  ltexprlem7  8662  addcanpr  8666  mulgt0sr  8723  map2psrpr  8728  supsrlem  8729  axrrecex  8781  letr  8910  recex  9396  lemul12b  9609  mulgt1  9611  ledivmulOLD  9626  fimaxre2  9698  lbreu  9700  nnrecgt0  9779  nnunb  9957  bndndx  9960  zeo  10093  uzind  10099  fzind  10105  fnn0ind  10106  lbzbi  10302  suprzcl2  10304  zmax  10309  rpnnen1lem5  10342  xrletr  10485  qbtwnre  10521  qsqueeze  10523  qextltlem  10524  xralrple  10527  xlesubadd  10578  supxrunb1  10633  icoshft  10753  fzen  10806  modadd1  10996  modmul1  10997  uzrdgfni  11016  seqcl2  11059  seqfveq2  11063  seqshft2  11067  monoord  11071  seqsplit  11074  seqf1olem1  11080  seqf1olem2  11081  seqid2  11087  seqhomo  11088  expnbnd  11225  faclbnd4lem4  11304  seqcoll  11396  sqeqd  11646  sqrmo  11732  cau3lem  11833  limsupbnd2  11952  lo1bdd2  11993  climuni  12021  rlimcn2  12059  mulcn2  12064  o1of2  12081  rlimo1  12085  lo1le  12120  isercolllem1  12133  iseralt  12152  isumrpcl  12297  cvgrat  12334  rpnnen2  12499  ruclem3  12506  sqr2irr  12522  dvds2lem  12536  dvdslelem  12568  divalglem8  12594  bitsinv1lem  12627  sadcaddlem  12643  smu01lem  12671  smueqlem  12676  bezoutlem4  12715  algcvga  12744  isprm3  12762  coprm  12774  coprmdvds2  12777  isprm5  12786  rpexp12i  12796  phibndlem  12833  dfphi2  12837  eulerthlem2  12845  odzdvds  12855  iserodd  12883  pclem  12886  pcpremul  12891  pcqcl  12904  pcdvdsb  12916  pcprmpw2  12929  pcaddlem  12931  pcmptcl  12934  pcfac  12942  prmpwdvds  12946  unbenlem  12950  prmreclem1  12958  4sqlem17  13003  vdwmc2  13021  vdwlem9  13031  vdwlem10  13032  vdwlem13  13035  vdwnnlem3  13039  ramcl  13071  mreiincl  13493  pospo  14102  dirge  14354  oddvdsnn0  14854  oddvds  14857  odcl2  14873  gexdvds  14890  sylow1lem1  14904  sylow2alem2  14924  sylow2a  14925  efgi2  15029  efgsrel  15038  efgs1b  15040  cyggex2  15178  pgpfac1lem2  15305  pgpfac1lem3a  15306  pgpfac1lem3  15307  pgpfac1lem5  15309  lssssr  15705  gzrngunitlem  16431  znunit  16512  frgpcyg  16522  lsmcss  16587  obselocv  16623  obslbs  16625  ordtrest2lem  16928  leordtval2  16937  lecldbas  16944  cncls  16998  cncnp  17004  cnpresti  17011  lmcnp  17027  cnt0  17069  isreg2  17100  cmpsublem  17121  cmpsub  17122  tgcmp  17123  dfcon2  17140  1stcfb  17166  2ndcctbss  17176  1stcelcls  17182  islly2  17205  dislly  17218  kgencn2  17247  txcnp  17309  txindis  17323  txcmplem1  17330  txlm  17337  xkohaus  17342  cnmptcom  17367  kqfvima  17416  isr0  17423  fgss2  17564  fbasrn  17574  filuni  17575  ufilmax  17597  isufil2  17598  cfinufil  17618  fmfnfmlem1  17644  fmfnfmlem2  17645  fmfnfmlem4  17647  fmfnfm  17648  fmco  17651  flimopn  17665  hausflim  17671  flimrest  17673  fclsopn  17704  flimfnfcls  17718  alexsubALTlem2  17737  alexsubALTlem3  17738  alexsubALT  17740  ptcmplem2  17742  symgtgp  17779  divstgplem  17798  tsmsres  17821  tsmsxplem1  17830  imasdsf1olem  17932  bldisj  17950  blss  17967  metcnp3  18081  ngptgp  18147  nrginvrcn  18197  nmoleub  18235  xrsmopn  18313  icccmplem3  18324  reconnlem2  18327  rectbntr0  18332  rescncf  18396  icoopnst  18432  iocopnst  18433  iccpnfcnv  18437  lebnumii  18459  nmoleub2lem  18590  nmhmcn  18596  fgcfil  18692  iscfil3  18694  iscau2  18698  iscau3  18699  iscau4  18700  iscmet3lem2  18713  cfilres  18717  caussi  18718  equivcfil  18720  equivcau  18721  caubl  18728  ivthlem2  18807  ivthlem3  18808  ovoliunlem2  18857  ovoliunnul  18861  ovolicc2lem3  18873  ioombl1lem4  18913  dyadmax  18948  dyadmbl  18950  volsup2  18955  itg2le  19089  itg2const2  19091  itg2seq  19092  itgsplitioo  19187  dvnres  19275  rolle  19332  c1lip1  19339  dvivthlem1  19350  lhop1  19356  dvcnvrelem1  19359  dvfsumrlim  19373  ply1divmo  19516  ig1peu  19552  plypf1  19589  coeaddlem  19625  fta1  19683  quotcan  19684  aalioulem4  19710  ulmcaulem  19766  ulmcn  19771  pilem2  19823  sincosq1lem  19860  sinq12gt0  19870  sinq12ge0  19871  sineq0  19884  tanord1  19894  lognegb  19938  logrec  20112  dcubic  20137  xrlimcnp  20258  o1cxp  20264  ftalem2  20306  ftalem3  20307  fsumdvdscom  20420  chtub  20446  vmasum  20450  bcmono  20511  bposlem3  20520  bposlem7  20524  lgsdir  20564  lgsqrlem2  20576  lgsdchr  20582  lgsquadlem2  20589  2sqlem6  20603  dchrisumlem3  20635  pntrsumbnd2  20711  pntpbnd1  20730  pntibnd  20737  pntlem3  20753  pntleml  20755  ex-natded5.3-2  20816  isgrpo  20856  opidon  20982  vacn  21260  ubthlem2  21443  htthlem  21490  normgt0  21699  shmodsi  21961  spansneleq  22142  h1datomi  22153  pjjsi  22272  nmcexi  22599  pjnormssi  22741  stm1add3i  22820  golem2  22845  cvnsym  22863  dmdmd  22873  mdslmd1lem1  22898  mdslmd1i  22902  mdexchi  22908  atcveq0  22921  superpos  22927  hatomistici  22935  atoml2i  22956  atcvat2i  22960  chirredlem1  22963  atcvat3i  22969  mdsymlem3  22978  mdsymlem5  22980  cdj3lem2b  23010  cdj3i  23014  ifeqeqx  23027  ballotlemfc0  23045  ballotlemfcc  23046  ballotlemfrceq  23081  subfacp1lem6  23121  iccllyscon  23186  cvmfolem  23215  cvmliftlem7  23227  cvmliftlem10  23230  eupath2  23309  ghomf1olem  23406  dedekind  23486  fundmpss  23524  dfon2lem3  23543  dfon2lem6  23546  axext4dist  23559  setlikess  23597  trpredtr  23635  trpredmintr  23636  dftrpred3g  23638  trpredrec  23643  frmin  23644  soseq  23656  wfrlem12  23669  frrlem5e  23691  frrlem11  23695  sltval2  23711  sltres  23719  axdenselem4  23740  axdenselem8  23744  axfelem6  23753  axfelem19  23766  dfrdg4  23896  brbtwn2  23941  colinearalg  23946  axcontlem10  24009  5segofs  24037  cgrextend  24039  segconeu  24042  btwncomim  24044  btwnswapid  24048  btwnintr  24050  btwnexch3  24051  btwndiff  24058  ifscgr  24075  cgrxfr  24086  btwnxfr  24087  lineext  24107  brofs2  24108  linecgr  24112  lineid  24114  idinside  24115  endofsegid  24116  btwnconn1lem13  24130  btwnconn3  24134  onsuct0  24288  limsucncmpi  24292  ubpar  24661  latdir  24695  intopcoaconc  24941  limfn3  24967  bwt2  24992  rdmob  25148  cmpmorp  25179  cmphmia  25198  cmphmib  25199  homgrf  25202  ismonc  25214  iepiclem  25223  isepic  25224  idfisf  25241  pgapspf2  25453  nbssntrs  25547  finminlem  25631  nn0prpwlem  25638  cldbnd  25644  clsint2  25647  reftr  25689  fnessref  25693  comppfsc  25707  neibastop3  25711  fgmin  25719  filbcmb  25832  nninfnub  25861  mettrifi  25873  geomcau  25875  istotbnd3  25895  sstotbnd2  25898  ismtybndlem  25930  heibor1lem  25933  heiborlem1  25935  heiborlem8  25942  heiborlem10  25944  heibor  25945  riscer  26019  crngohomfo  26031  keridl  26057  ispridl2  26063  ispridlc  26095  fphpdo  26300  icodiamlt  26305  pellexlem5  26318  pellexlem6  26319  jm2.26lem3  26494  dfac21  26564  unxpwdom3  26656  ordpss  27054  stoweidlem34  27183  19.41rg  27588  pwtrOLD  27868  ax10lem17ALT  28391  a12study10  28404  a12study10n  28405  ax9lem17  28424  lsatcveq0  28490  eqlkr3  28559  atlatmstc  28777  atlrelat1  28779  hlrelat2  28860  intnatN  28864  cvrexchlem  28876  cvratlem  28878  cvrat2  28886  atltcvr  28892  cvrat3  28899  cvrat4  28900  ps-1  28934  ps-2  28935  lplnnle2at  28998  lvolnle3at  29039  2llnma3r  29245  cdlemblem  29250  pmapjoin  29309  elpcliN  29350  lhpmcvr4N  29483  4atexlemnclw  29527  trlnidatb  29634  cdlemc4  29651  cdlemd3  29657  cdleme3g  29691  cdleme7d  29703  cdleme11c  29718  cdleme11dN  29719  cdleme21b  29783  cdleme21c  29784  cdleme21i  29792  cdleme22b  29798  cdleme35fnpq  29906  cdlemf1  30018  trlord  30026  cdlemg6c  30077  dihglblem6  30798  dochlkr  30843  dochkrshp  30844  dihjat1lem  30886  dochexmidlem5  30922  dochexmidlem8  30925
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator