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

Theorem syld 43
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 43 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 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 39 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  3syld  54  sylsyld  55  nsyld  135  pm2.61d  153  sylibd  207  sylbid  208  sylibrd  227  sylbird  228  syland  469  alrimdd  1785  cbv1hOLD  1976  ax12olem3  2008  ax10o2  2025  dvelimvOLD  2029  dral1OLD  2059  sbequi  2112  sbequiOLD  2116  sbiedOLD  2153  dral1-o  2233  ax11indalem  2276  ax11inda2ALT  2277  trel3  4312  poss  4507  sess2  4553  wefrc  4578  wereu2  4581  ordelord  4605  oninton  4782  orduniorsuc  4812  limuni3  4834  tfindsg  4842  limom  4862  funun  5497  ssimaex  5790  f1dmex  5973  f1imass  6012  soisoi  6050  isores3  6057  isofrlem  6062  isoselem  6063  weniso  6077  f1o2ndf1  6456  soxp  6461  riotasv3dOLD  6601  smoel  6624  smogt  6631  tfrlem9  6648  tz7.49  6704  seqomlem1  6709  abianfp  6718  odi  6824  omass  6825  omeulem2  6828  oeordsuc  6839  oeeulem  6846  ertr  6922  swoord2  6937  ecopovtrn  7009  domtriord  7255  2pwuninel  7264  onomeneq  7298  unxpdomlem2  7316  isinf  7324  pssnn  7329  findcard3  7352  frfi  7354  unblem3  7363  dffi3  7438  inf3lem3  7587  inf3lem5  7589  noinfep  7616  cantnfle  7628  cantnfp1lem3  7638  en3lplem1  7672  rankxpsuc  7808  tcrank  7810  ficardom  7850  carduni  7870  infxpenlem  7897  dfac8alem  7912  ac10ct  7917  ween  7918  alephdom  7964  alephle  7971  iscard3  7976  alephfp  7991  cdainf  8074  pwsdompw  8086  infdif  8091  cfslbn  8149  cofsmo  8151  cfsmolem  8152  cfcof  8156  fin1a2s  8296  domtriomlem  8324  ac6num  8361  zorn2lem3  8380  axdclem2  8402  imadomg  8414  iundom2g  8417  ficard  8442  fpwwe2lem8  8514  fpwwe2  8520  gchaclem  8547  tskr1om2  8645  inar1  8652  tskord  8657  tskuni  8660  grudomon  8694  grur1a  8696  grur1  8697  addnidpi  8780  ltexnq  8854  genpnnp  8884  addclprlem2  8896  mulclprlem  8898  psslinpr  8910  ltaddpr2  8914  ltexprlem6  8920  ltexprlem7  8921  addcanpr  8925  mulgt0sr  8982  map2psrpr  8987  supsrlem  8988  axrrecex  9040  letr  9169  recex  9656  lemul12b  9869  mulgt1  9871  ledivmulOLD  9886  fimaxre2  9958  lbreu  9960  nnrecgt0  10039  nnunb  10219  bndndx  10222  zeo  10357  uzind  10363  fzind  10370  fnn0ind  10371  lbzbi  10566  suprzcl2  10568  zmax  10573  rpnnen1lem5  10606  xrletr  10750  qbtwnre  10787  qsqueeze  10789  qextltlem  10790  xralrple  10793  xlesubadd  10844  supxrunb1  10900  icoshft  11021  fzen  11074  modadd1  11280  modmul1  11281  uzrdgfni  11300  seqcl2  11343  seqfveq2  11347  seqshft2  11351  monoord  11355  seqsplit  11358  seqf1olem1  11364  seqf1olem2  11365  seqid2  11371  seqhomo  11372  expnbnd  11510  faclbnd4lem4  11589  seqcoll  11714  sqeqd  11973  sqrmo  12059  cau3lem  12160  limsupbnd2  12279  lo1bdd2  12320  climuni  12348  rlimcn2  12386  mulcn2  12391  o1of2  12408  rlimo1  12412  lo1le  12447  isercolllem1  12460  iseralt  12480  isumrpcl  12625  cvgrat  12662  rpnnen2  12827  ruclem3  12834  sqr2irr  12850  dvds2lem  12864  dvdslelem  12896  divalglem8  12922  bitsinv1lem  12955  sadcaddlem  12971  smu01lem  12999  smueqlem  13004  bezoutlem4  13043  algcvga  13072  isprm3  13090  coprm  13102  coprmdvds2  13105  isprm5  13114  rpexp12i  13124  phibndlem  13161  dfphi2  13165  eulerthlem2  13173  odzdvds  13183  iserodd  13211  pclem  13214  pcpremul  13219  pcqcl  13232  pcdvdsb  13244  pcprmpw2  13257  pcaddlem  13259  pcmptcl  13262  pcfac  13270  prmpwdvds  13274  unbenlem  13278  prmreclem1  13286  4sqlem17  13331  vdwmc2  13349  vdwlem9  13359  vdwlem10  13360  vdwlem13  13363  vdwnnlem3  13367  ramcl  13399  mreiincl  13823  pospo  14432  dirge  14684  oddvdsnn0  15184  oddvds  15187  odcl2  15203  gexdvds  15220  sylow1lem1  15234  sylow2alem2  15254  sylow2a  15255  efgi2  15359  efgsrel  15368  efgs1b  15370  cyggex2  15508  pgpfac1lem2  15635  pgpfac1lem3a  15636  pgpfac1lem3  15637  pgpfac1lem5  15639  lssssr  16031  gzrngunitlem  16765  znunit  16846  frgpcyg  16856  lsmcss  16921  obselocv  16957  obslbs  16959  ordtrest2lem  17269  leordtval2  17278  lecldbas  17285  cncls  17340  cncnp  17346  cnpresti  17354  lmcnp  17370  cnt0  17412  isreg2  17443  cmpsublem  17464  cmpsub  17465  tgcmp  17466  bwth  17475  dfcon2  17484  1stcfb  17510  2ndcctbss  17520  1stcelcls  17526  islly2  17549  dislly  17562  kgencn2  17591  txcnp  17654  txindis  17668  txcmplem1  17675  txlm  17682  xkohaus  17687  cnmptcom  17712  kqfvima  17764  isr0  17771  fgss2  17908  fbasrn  17918  filuni  17919  ufilmax  17941  isufil2  17942  cfinufil  17962  fmfnfmlem1  17988  fmfnfmlem2  17989  fmfnfmlem4  17991  fmfnfm  17992  fmco  17995  flimopn  18009  hausflim  18015  flimrest  18017  fclsopn  18048  flimfnfcls  18062  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALT  18084  ptcmplem2  18086  cnextcn  18100  symgtgp  18133  divstgplem  18152  tsmsres  18175  tsmsxplem1  18184  isucn2  18311  imasdsf1olem  18405  bldisj  18430  blssps  18456  blss  18457  metcnp3  18572  ngptgp  18679  nrginvrcn  18729  nmoleub  18767  xrsmopn  18845  icccmplem3  18857  reconnlem2  18860  rectbntr0  18865  rescncf  18929  icoopnst  18966  iocopnst  18967  iccpnfcnv  18971  lebnumii  18993  nmoleub2lem  19124  nmhmcn  19130  fgcfil  19226  iscfil3  19228  iscau2  19232  iscau3  19233  iscau4  19234  iscmet3lem2  19247  cfilres  19251  caussi  19252  equivcfil  19254  equivcau  19255  caubl  19262  ivthlem2  19351  ivthlem3  19352  ovoliunlem2  19401  ovoliunnul  19405  ovolicc2lem3  19417  ioombl1lem4  19457  dyadmax  19492  dyadmbl  19494  volsup2  19499  itg2le  19633  itg2const2  19635  itg2seq  19636  itgsplitioo  19731  dvnres  19819  rolle  19876  c1lip1  19883  dvivthlem1  19894  lhop1  19900  dvcnvrelem1  19903  dvfsumrlim  19917  ply1divmo  20060  ig1peu  20096  plypf1  20133  coeaddlem  20169  fta1  20227  quotcan  20228  aalioulem4  20254  ulmcaulem  20312  ulmcn  20317  pilem2  20370  sincosq1lem  20407  sinq12gt0  20417  sinq12ge0  20418  sineq0  20431  tanord1  20441  lognegb  20486  logrec  20663  dcubic  20688  xrlimcnp  20809  o1cxp  20815  ftalem2  20858  ftalem3  20859  fsumdvdscom  20972  chtub  20998  vmasum  21002  bcmono  21063  bposlem3  21072  bposlem7  21076  lgsdir  21116  lgsqrlem2  21128  lgsdchr  21134  lgsquadlem2  21141  2sqlem6  21155  dchrisumlem3  21187  pntrsumbnd2  21263  pntpbnd1  21282  pntibnd  21289  pntlem3  21305  pntleml  21307  redwlk  21608  fargshiftf1  21626  constr3trllem2  21640  4cycl4dv  21656  vdusgra0nedg  21681  usgravd0nedg  21685  eupath2  21704  isgrpo  21786  opidon  21912  vacn  22192  ubthlem2  22375  htthlem  22422  normgt0  22631  shmodsi  22893  spansneleq  23074  h1datomi  23085  pjjsi  23204  nmcexi  23531  pjnormssi  23673  stm1add3i  23752  golem2  23777  cvnsym  23795  dmdmd  23805  mdslmd1lem1  23830  mdslmd1i  23834  mdexchi  23840  atcveq0  23853  superpos  23859  hatomistici  23867  atoml2i  23888  atcvat2i  23892  chirredlem1  23895  atcvat3i  23901  mdsymlem3  23910  mdsymlem5  23912  cdj3lem2b  23942  cdj3i  23946  supssd  24100  resspos  24189  resstos  24190  tpr2rico  24312  xrge0iifcnv  24321  ballotlemfc0  24752  ballotlemfcc  24753  subfacp1lem6  24873  iccllyscon  24939  cvmfolem  24968  cvmliftlem7  24980  cvmliftlem10  24983  ghomf1olem  25107  dedekind  25189  fprodss  25276  fundmpss  25392  dfon2lem3  25414  dfon2lem6  25417  axext4dist  25430  setlikess  25472  trpredtr  25510  trpredmintr  25511  dftrpred3g  25513  trpredrec  25518  frmin  25519  soseq  25531  wfrlem12  25551  frrlem5e  25592  frrlem11  25596  sltval2  25613  sltres  25621  nodenselem4  25641  nodenselem8  25645  nobndlem6  25654  dfrdg4  25797  brbtwn2  25846  colinearalg  25851  axcontlem10  25914  5segofs  25942  cgrextend  25944  segconeu  25947  btwncomim  25949  btwnswapid  25953  btwnintr  25955  btwnexch3  25956  btwndiff  25963  ifscgr  25980  cgrxfr  25991  btwnxfr  25992  lineext  26012  brofs2  26013  linecgr  26017  lineid  26019  idinside  26020  endofsegid  26021  btwnconn1lem13  26035  btwnconn3  26039  onsuct0  26193  limsucncmpi  26197  ltflcei  26241  mblfinlem2  26246  mblfinlem3  26247  itg2addnclem  26258  itg2addnclem2  26259  itg2gt0cn  26262  ftc1anclem5  26286  ftc1anclem6  26287  finminlem  26323  nn0prpwlem  26327  cldbnd  26331  clsint2  26334  reftr  26371  fnessref  26375  comppfsc  26389  neibastop3  26393  fgmin  26401  filbcmb  26444  nninfnub  26457  mettrifi  26465  geomcau  26467  istotbnd3  26482  sstotbnd2  26485  ismtybndlem  26517  heibor1lem  26520  heiborlem1  26522  heiborlem8  26529  heiborlem10  26531  heibor  26532  riscer  26606  crngohomfo  26618  keridl  26644  ispridl2  26650  ispridlc  26682  fphpdo  26880  icodiamlt  26885  pellexlem5  26898  pellexlem6  26899  jm2.26lem3  27074  dfac21  27143  unxpwdom3  27235  ordpss  27632  stoweidlem34  27761  ltsubnn0  28108  elfz2z  28116  elfzmlbm  28117  elfzmlbp  28118  elfz0fzfz0  28125  ubmelm1fzo  28138  fzo1fzo0n0  28139  fzofzim  28147  wrdlenge2n0  28196  swrdnd  28204  swrdvalodmlem1  28209  swrdvalodm2  28210  swrdswrdlem  28220  swrdswrd  28221  swrdccatin12lem3a  28230  swrdccatin12lem3b  28231  swrdccatin12lem4  28235  swrdccat3a  28239  swrdccat3blem  28240  2cshw1lem1  28270  2cshw1lem2  28271  2cshwmod  28279  cshweqdif2s  28293  usg2wlkeq  28330  usgra2adedgspthlem2  28340  usg2wotspth  28404  usgravd00  28424  19.41rg  28699  dvelimvNEW7  29524  dral1NEW7  29555  cbv1hwAUX7  29573  sbiedNEW7  29602  sbequiNEW7  29641  ax7w15lemxAUX7  29728  cbv1hOLD7  29781  lsatcveq0  29892  eqlkr3  29961  atlatmstc  30179  atlrelat1  30181  hlrelat2  30262  intnatN  30266  cvrexchlem  30278  cvratlem  30280  cvrat2  30288  atltcvr  30294  cvrat3  30301  cvrat4  30302  ps-1  30336  ps-2  30337  lplnnle2at  30400  lvolnle3at  30441  2llnma3r  30647  cdlemblem  30652  pmapjoin  30711  elpcliN  30752  lhpmcvr4N  30885  4atexlemnclw  30929  trlnidatb  31036  cdlemc4  31053  cdlemd3  31059  cdleme3g  31093  cdleme7d  31105  cdleme11c  31120  cdleme11dN  31121  cdleme21b  31185  cdleme21c  31186  cdleme21i  31194  cdleme22b  31200  cdleme35fnpq  31308  cdlemf1  31420  trlord  31428  cdlemg6c  31479  dihglblem6  32200  dochlkr  32245  dochkrshp  32246  dihjat1lem  32288  dochexmidlem5  32324  dochexmidlem8  32327
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator