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  1748  dvelimv  1879  ax10lem6  1883  dral1  1905  cbv1h  1918  sbied  1976  sbequi  1999  dral1-o  2093  ax11indalem  2136  ax11inda2ALT  2137  trel3  4121  poss  4316  sess2  4362  wefrc  4387  wereu2  4390  ordelord  4414  oninton  4591  orduniorsuc  4621  limuni3  4643  tfindsg  4651  limom  4671  funun  5296  ssimaex  5584  f1dmex  5751  f1imass  5788  soisoi  5825  isores3  5832  isofrlem  5837  isoselem  5838  weniso  5852  soxp  6228  riotasv3dOLD  6354  smoel  6377  smogt  6384  tfrlem9  6401  tz7.49  6457  seqomlem1  6462  abianfp  6471  odi  6577  omass  6578  omeulem2  6581  oeordsuc  6592  oeeulem  6599  ertr  6675  swoord2  6690  ecopovtrn  6761  domtriord  7007  2pwuninel  7016  onomeneq  7050  unxpdomlem2  7068  isinf  7076  pssnn  7081  findcard3  7100  frfi  7102  unblem3  7111  dffi3  7184  inf3lem3  7331  inf3lem5  7333  noinfep  7360  cantnfle  7372  cantnfp1lem3  7382  en3lplem1  7416  rankxpsuc  7552  tcrank  7554  ficardom  7594  carduni  7614  infxpenlem  7641  dfac8alem  7656  ac10ct  7661  ween  7662  alephdom  7708  alephle  7715  iscard3  7720  alephfp  7735  cdainf  7818  pwsdompw  7830  infdif  7835  cfslbn  7893  cofsmo  7895  cfsmolem  7896  cfcof  7900  fin1a2s  8040  domtriomlem  8068  ac6num  8106  zorn2lem3  8125  axdclem2  8147  imadomg  8159  iundom2g  8162  ficard  8187  fpwwe2lem8  8259  fpwwe2  8265  gchaclem  8292  tskr1om2  8390  inar1  8397  tskord  8402  tskuni  8405  grudomon  8439  grur1a  8441  grur1  8442  addnidpi  8525  ltexnq  8599  genpnnp  8629  addclprlem2  8641  mulclprlem  8643  psslinpr  8655  ltaddpr2  8659  ltexprlem6  8665  ltexprlem7  8666  addcanpr  8670  mulgt0sr  8727  map2psrpr  8732  supsrlem  8733  axrrecex  8785  letr  8914  recex  9400  lemul12b  9613  mulgt1  9615  ledivmulOLD  9630  fimaxre2  9702  lbreu  9704  nnrecgt0  9783  nnunb  9961  bndndx  9964  zeo  10097  uzind  10103  fzind  10110  fnn0ind  10111  lbzbi  10306  suprzcl2  10308  zmax  10313  rpnnen1lem5  10346  xrletr  10489  qbtwnre  10526  qsqueeze  10528  qextltlem  10529  xralrple  10532  xlesubadd  10583  supxrunb1  10638  icoshft  10758  fzen  10811  modadd1  11001  modmul1  11002  uzrdgfni  11021  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqf1olem1  11085  seqf1olem2  11086  seqid2  11092  seqhomo  11093  expnbnd  11230  faclbnd4lem4  11309  seqcoll  11401  sqeqd  11651  sqrmo  11737  cau3lem  11838  limsupbnd2  11957  lo1bdd2  11998  climuni  12026  rlimcn2  12064  mulcn2  12069  o1of2  12086  rlimo1  12090  lo1le  12125  isercolllem1  12138  iseralt  12157  isumrpcl  12302  cvgrat  12339  rpnnen2  12504  ruclem3  12511  sqr2irr  12527  dvds2lem  12541  dvdslelem  12573  divalglem8  12599  bitsinv1lem  12632  sadcaddlem  12648  smu01lem  12676  smueqlem  12681  bezoutlem4  12720  algcvga  12749  isprm3  12767  coprm  12779  coprmdvds2  12782  isprm5  12791  rpexp12i  12801  phibndlem  12838  dfphi2  12842  eulerthlem2  12850  odzdvds  12860  iserodd  12888  pclem  12891  pcpremul  12896  pcqcl  12909  pcdvdsb  12921  pcprmpw2  12934  pcaddlem  12936  pcmptcl  12939  pcfac  12947  prmpwdvds  12951  unbenlem  12955  prmreclem1  12963  4sqlem17  13008  vdwmc2  13026  vdwlem9  13036  vdwlem10  13037  vdwlem13  13040  vdwnnlem3  13044  ramcl  13076  mreiincl  13498  pospo  14107  dirge  14359  oddvdsnn0  14859  oddvds  14862  odcl2  14878  gexdvds  14895  sylow1lem1  14909  sylow2alem2  14929  sylow2a  14930  efgi2  15034  efgsrel  15043  efgs1b  15045  cyggex2  15183  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem5  15314  lssssr  15710  gzrngunitlem  16436  znunit  16517  frgpcyg  16527  lsmcss  16592  obselocv  16628  obslbs  16630  ordtrest2lem  16933  leordtval2  16942  lecldbas  16949  cncls  17003  cncnp  17009  cnpresti  17016  lmcnp  17032  cnt0  17074  isreg2  17105  cmpsublem  17126  cmpsub  17127  tgcmp  17128  dfcon2  17145  1stcfb  17171  2ndcctbss  17181  1stcelcls  17187  islly2  17210  dislly  17223  kgencn2  17252  txcnp  17314  txindis  17328  txcmplem1  17335  txlm  17342  xkohaus  17347  cnmptcom  17372  kqfvima  17421  isr0  17428  fgss2  17569  fbasrn  17579  filuni  17580  ufilmax  17602  isufil2  17603  cfinufil  17623  fmfnfmlem1  17649  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  fmco  17656  flimopn  17670  hausflim  17676  flimrest  17678  fclsopn  17709  flimfnfcls  17723  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALT  17745  ptcmplem2  17747  symgtgp  17784  divstgplem  17803  tsmsres  17826  tsmsxplem1  17835  imasdsf1olem  17937  bldisj  17955  blss  17972  metcnp3  18086  ngptgp  18152  nrginvrcn  18202  nmoleub  18240  xrsmopn  18318  icccmplem3  18329  reconnlem2  18332  rectbntr0  18337  rescncf  18401  icoopnst  18437  iocopnst  18438  iccpnfcnv  18442  lebnumii  18464  nmoleub2lem  18595  nmhmcn  18601  fgcfil  18697  iscfil3  18699  iscau2  18703  iscau3  18704  iscau4  18705  iscmet3lem2  18718  cfilres  18722  caussi  18723  equivcfil  18725  equivcau  18726  caubl  18733  ivthlem2  18812  ivthlem3  18813  ovoliunlem2  18862  ovoliunnul  18866  ovolicc2lem3  18878  ioombl1lem4  18918  dyadmax  18953  dyadmbl  18955  volsup2  18960  itg2le  19094  itg2const2  19096  itg2seq  19097  itgsplitioo  19192  dvnres  19280  rolle  19337  c1lip1  19344  dvivthlem1  19355  lhop1  19361  dvcnvrelem1  19364  dvfsumrlim  19378  ply1divmo  19521  ig1peu  19557  plypf1  19594  coeaddlem  19630  fta1  19688  quotcan  19689  aalioulem4  19715  ulmcaulem  19771  ulmcn  19776  pilem2  19828  sincosq1lem  19865  sinq12gt0  19875  sinq12ge0  19876  sineq0  19889  tanord1  19899  lognegb  19943  logrec  20117  dcubic  20142  xrlimcnp  20263  o1cxp  20269  ftalem2  20311  ftalem3  20312  fsumdvdscom  20425  chtub  20451  vmasum  20455  bcmono  20516  bposlem3  20525  bposlem7  20529  lgsdir  20569  lgsqrlem2  20581  lgsdchr  20587  lgsquadlem2  20594  2sqlem6  20608  dchrisumlem3  20640  pntrsumbnd2  20716  pntpbnd1  20735  pntibnd  20742  pntlem3  20758  pntleml  20760  ex-natded5.3-2  20795  isgrpo  20863  opidon  20989  vacn  21267  ubthlem2  21450  htthlem  21497  normgt0  21706  shmodsi  21968  spansneleq  22149  h1datomi  22160  pjjsi  22279  nmcexi  22606  pjnormssi  22748  stm1add3i  22827  golem2  22852  cvnsym  22870  dmdmd  22880  mdslmd1lem1  22905  mdslmd1i  22909  mdexchi  22915  atcveq0  22928  superpos  22934  hatomistici  22942  atoml2i  22963  atcvat2i  22967  chirredlem1  22970  atcvat3i  22976  mdsymlem3  22985  mdsymlem5  22987  cdj3lem2b  23017  cdj3i  23021  ifeqeqx  23034  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemfrceq  23087  bisimpd  23120  supssd  23248  cnre2csqlem  23294  tpr2rico  23296  xrge0iifcnv  23315  sigaclci  23493  subfacp1lem6  23716  iccllyscon  23781  cvmfolem  23810  cvmliftlem7  23822  cvmliftlem10  23825  eupath2  23904  ghomf1olem  24001  dedekind  24082  fundmpss  24122  dfon2lem3  24141  dfon2lem6  24144  axext4dist  24157  setlikess  24195  trpredtr  24233  trpredmintr  24234  dftrpred3g  24236  trpredrec  24241  frmin  24242  soseq  24254  wfrlem12  24267  frrlem5e  24289  frrlem11  24293  sltval2  24310  sltres  24318  nodenselem4  24338  nodenselem8  24342  nobndlem6  24351  dfrdg4  24488  brbtwn2  24533  colinearalg  24538  axcontlem10  24601  5segofs  24629  cgrextend  24631  segconeu  24634  btwncomim  24636  btwnswapid  24640  btwnintr  24642  btwnexch3  24643  btwndiff  24650  ifscgr  24667  cgrxfr  24678  btwnxfr  24679  lineext  24699  brofs2  24700  linecgr  24704  lineid  24706  idinside  24707  endofsegid  24708  btwnconn1lem13  24722  btwnconn3  24726  onsuct0  24880  limsucncmpi  24884  ubpar  25261  latdir  25295  intopcoaconc  25541  limfn3  25567  bwt2  25592  rdmob  25748  cmpmorp  25779  cmphmia  25798  cmphmib  25799  homgrf  25802  ismonc  25814  iepiclem  25823  isepic  25824  idfisf  25841  pgapspf2  26053  nbssntrs  26147  finminlem  26231  nn0prpwlem  26238  cldbnd  26244  clsint2  26247  reftr  26289  fnessref  26293  comppfsc  26307  neibastop3  26311  fgmin  26319  filbcmb  26432  nninfnub  26461  mettrifi  26473  geomcau  26475  istotbnd3  26495  sstotbnd2  26498  ismtybndlem  26530  heibor1lem  26533  heiborlem1  26535  heiborlem8  26542  heiborlem10  26544  heibor  26545  riscer  26619  crngohomfo  26631  keridl  26657  ispridl2  26663  ispridlc  26695  fphpdo  26900  icodiamlt  26905  pellexlem5  26918  pellexlem6  26919  jm2.26lem3  27094  dfac21  27164  unxpwdom3  27256  ordpss  27654  stoweidlem34  27783  19.41rg  28316  pwtrOLD  28599  ax10lem17ALT  29123  a12study10  29136  a12study10n  29137  ax9lem17  29156  lsatcveq0  29222  eqlkr3  29291  atlatmstc  29509  atlrelat1  29511  hlrelat2  29592  intnatN  29596  cvrexchlem  29608  cvratlem  29610  cvrat2  29618  atltcvr  29624  cvrat3  29631  cvrat4  29632  ps-1  29666  ps-2  29667  lplnnle2at  29730  lvolnle3at  29771  2llnma3r  29977  cdlemblem  29982  pmapjoin  30041  elpcliN  30082  lhpmcvr4N  30215  4atexlemnclw  30259  trlnidatb  30366  cdlemc4  30383  cdlemd3  30389  cdleme3g  30423  cdleme7d  30435  cdleme11c  30450  cdleme11dN  30451  cdleme21b  30515  cdleme21c  30516  cdleme21i  30524  cdleme22b  30530  cdleme35fnpq  30638  cdlemf1  30750  trlord  30758  cdlemg6c  30809  dihglblem6  31530  dochlkr  31575  dochkrshp  31576  dihjat1lem  31618  dochexmidlem5  31654  dochexmidlem8  31657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator