MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld Structured version   GIF 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 𝜑 added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace 𝜑 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 (𝜑 → (𝜓𝜒))
syld.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
syld (𝜑 → (𝜓𝜃))

Proof of Theorem syld
StepHypRef Expression
1 syld.1 . 2 (𝜑 → (𝜓𝜒))
2 syld.2 . . 3 (𝜑 → (𝜒𝜃))
32a1d 24 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpdd 39 1 (𝜑 → (𝜓𝜃))
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  1787  cbv1hOLD  1979  ax12olem3  2011  ax10o2  2028  dvelimvOLD  2032  dral1OLD  2062  sbequi  2115  sbequiOLD  2119  sbiedOLD  2158  dral1-o  2238  ax11indalem  2281  ax11inda2ALT  2282  trel3  4341  poss  4540  sess2  4586  wefrc  4611  wereu2  4614  ordelord  4638  oninton  4815  orduniorsuc  4845  limuni3  4867  tfindsg  4875  limom  4895  funun  5530  ssimaex  5824  f1dmex  6007  f1imass  6046  soisoi  6084  isores3  6091  isofrlem  6096  isoselem  6097  weniso  6111  f1o2ndf1  6490  soxp  6495  riotasv3dOLD  6635  smoel  6658  smogt  6665  tfrlem9  6682  tz7.49  6738  seqomlem1  6743  abianfp  6752  odi  6858  omass  6859  omeulem2  6862  oeordsuc  6873  oeeulem  6880  ertr  6956  swoord2  6971  ecopovtrn  7043  domtriord  7289  2pwuninel  7298  onomeneq  7332  unxpdomlem2  7350  isinf  7358  pssnn  7363  findcard3  7386  frfi  7388  unblem3  7397  dffi3  7472  inf3lem3  7621  inf3lem5  7623  noinfep  7650  cantnfle  7662  cantnfp1lem3  7672  en3lplem1  7706  rankxpsuc  7844  tcrank  7846  ficardom  7886  carduni  7906  infxpenlem  7933  dfac8alem  7948  ac10ct  7953  ween  7954  alephdom  8000  alephle  8007  iscard3  8012  alephfp  8027  cdainf  8110  pwsdompw  8122  infdif  8127  cfslbn  8185  cofsmo  8187  cfsmolem  8188  cfcof  8192  fin1a2s  8332  domtriomlem  8360  ac6num  8397  zorn2lem3  8416  axdclem2  8438  imadomg  8450  iundom2g  8453  ficard  8478  fpwwe2lem8  8550  fpwwe2  8556  gchaclem  8591  tskr1om2  8681  inar1  8688  tskord  8693  tskuni  8696  grudomon  8730  grur1a  8732  grur1  8733  addnidpi  8816  ltexnq  8890  genpnnp  8920  addclprlem2  8932  mulclprlem  8934  psslinpr  8946  ltaddpr2  8950  ltexprlem6  8956  ltexprlem7  8957  addcanpr  8961  mulgt0sr  9018  map2psrpr  9023  supsrlem  9024  axrrecex  9076  letr  9205  recex  9692  lemul12b  9905  mulgt1  9907  ledivmulOLD  9922  fimaxre2  9994  lbreu  9996  nnrecgt0  10075  nnunb  10255  bndndx  10258  zeo  10393  uzind  10399  fzind  10406  fnn0ind  10407  lbzbi  10602  suprzcl2  10604  zmax  10609  rpnnen1lem5  10642  xrletr  10786  qbtwnre  10823  qsqueeze  10825  qextltlem  10826  xralrple  10829  xlesubadd  10880  supxrunb1  10936  icoshft  11057  fzen  11110  modadd1  11316  modmul1  11317  uzrdgfni  11336  seqcl2  11379  seqfveq2  11383  seqshft2  11387  monoord  11391  seqsplit  11394  seqf1olem1  11400  seqf1olem2  11401  seqid2  11407  seqhomo  11408  expnbnd  11546  faclbnd4lem4  11625  seqcoll  11750  sqeqd  12009  sqrmo  12095  cau3lem  12196  limsupbnd2  12315  lo1bdd2  12356  climuni  12384  rlimcn2  12422  mulcn2  12427  o1of2  12444  rlimo1  12448  lo1le  12483  isercolllem1  12496  iseralt  12516  isumrpcl  12661  cvgrat  12698  rpnnen2  12863  ruclem3  12870  sqr2irr  12886  dvds2lem  12900  dvdslelem  12932  divalglem8  12958  bitsinv1lem  12991  sadcaddlem  13007  smu01lem  13035  smueqlem  13040  bezoutlem4  13079  algcvga  13108  isprm3  13126  coprm  13138  coprmdvds2  13141  isprm5  13150  rpexp12i  13160  phibndlem  13197  dfphi2  13201  eulerthlem2  13209  odzdvds  13219  iserodd  13247  pclem  13250  pcpremul  13255  pcqcl  13268  pcdvdsb  13280  pcprmpw2  13293  pcaddlem  13295  pcmptcl  13298  pcfac  13306  prmpwdvds  13310  unbenlem  13314  prmreclem1  13322  4sqlem17  13367  vdwmc2  13385  vdwlem9  13395  vdwlem10  13396  vdwlem13  13399  vdwnnlem3  13403  ramcl  13435  mreiincl  13859  pospo  14468  dirge  14720  oddvdsnn0  15220  oddvds  15223  odcl2  15239  gexdvds  15256  sylow1lem1  15270  sylow2alem2  15290  sylow2a  15291  efgi2  15395  efgsrel  15404  efgs1b  15406  cyggex2  15544  pgpfac1lem2  15671  pgpfac1lem3a  15672  pgpfac1lem3  15673  pgpfac1lem5  15675  lssssr  16067  gzrngunitlem  16801  znunit  16882  frgpcyg  16892  lsmcss  16957  obselocv  16993  obslbs  16995  ordtrest2lem  17305  leordtval2  17314  lecldbas  17321  cncls  17376  cncnp  17382  cnpresti  17390  lmcnp  17406  cnt0  17448  isreg2  17479  cmpsublem  17500  cmpsub  17501  tgcmp  17502  bwth  17511  dfcon2  17520  1stcfb  17546  2ndcctbss  17556  1stcelcls  17562  islly2  17585  dislly  17598  kgencn2  17627  txcnp  17690  txindis  17704  txcmplem1  17711  txlm  17718  xkohaus  17723  cnmptcom  17748  kqfvima  17800  isr0  17807  fgss2  17944  fbasrn  17954  filuni  17955  ufilmax  17977  isufil2  17978  cfinufil  17998  fmfnfmlem1  18024  fmfnfmlem2  18025  fmfnfmlem4  18027  fmfnfm  18028  fmco  18031  flimopn  18045  hausflim  18051  flimrest  18053  fclsopn  18084  flimfnfcls  18098  alexsubALTlem2  18117  alexsubALTlem3  18118  alexsubALT  18120  ptcmplem2  18122  cnextcn  18136  symgtgp  18169  divstgplem  18188  tsmsres  18211  tsmsxplem1  18220  isucn2  18347  imasdsf1olem  18441  bldisj  18466  blssps  18492  blss  18493  metcnp3  18608  ngptgp  18715  nrginvrcn  18765  nmoleub  18803  xrsmopn  18881  icccmplem3  18893  reconnlem2  18896  rectbntr0  18901  rescncf  18965  icoopnst  19002  iocopnst  19003  iccpnfcnv  19007  lebnumii  19029  nmoleub2lem  19160  nmhmcn  19166  fgcfil  19262  iscfil3  19264  iscau2  19268  iscau3  19269  iscau4  19270  iscmet3lem2  19283  cfilres  19287  caussi  19288  equivcfil  19290  equivcau  19291  caubl  19298  ivthlem2  19387  ivthlem3  19388  ovoliunlem2  19437  ovoliunnul  19441  ovolicc2lem3  19453  ioombl1lem4  19493  dyadmax  19528  dyadmbl  19530  volsup2  19535  itg2le  19667  itg2const2  19669  itg2seq  19670  itgsplitioo  19765  dvnres  19855  rolle  19912  c1lip1  19919  dvivthlem1  19930  lhop1  19936  dvcnvrelem1  19939  dvfsumrlim  19953  ply1divmo  20096  ig1peu  20132  plypf1  20169  coeaddlem  20205  fta1  20263  quotcan  20264  aalioulem4  20290  ulmcaulem  20348  ulmcn  20353  pilem2  20406  sincosq1lem  20443  sinq12gt0  20453  sinq12ge0  20454  sineq0  20467  tanord1  20477  lognegb  20522  logrec  20699  dcubic  20724  xrlimcnp  20845  o1cxp  20851  ftalem2  20894  ftalem3  20895  fsumdvdscom  21008  chtub  21034  vmasum  21038  bcmono  21099  bposlem3  21108  bposlem7  21112  lgsdir  21152  lgsqrlem2  21164  lgsdchr  21170  lgsquadlem2  21177  2sqlem6  21191  dchrisumlem3  21223  pntrsumbnd2  21299  pntpbnd1  21318  pntibnd  21325  pntlem3  21341  pntleml  21343  redwlk  21644  fargshiftf1  21662  constr3trllem2  21676  4cycl4dv  21692  vdusgra0nedg  21717  usgravd0nedg  21721  eupath2  21740  ex-natded5.3-2  21754  isgrpo  21822  opidon  21948  vacn  22228  ubthlem2  22411  htthlem  22458  normgt0  22667  shmodsi  22929  spansneleq  23110  h1datomi  23121  pjjsi  23240  nmcexi  23567  pjnormssi  23709  stm1add3i  23788  golem2  23813  cvnsym  23831  dmdmd  23841  mdslmd1lem1  23866  mdslmd1i  23870  mdexchi  23876  atcveq0  23889  superpos  23895  hatomistici  23903  atoml2i  23924  atcvat2i  23928  chirredlem1  23931  atcvat3i  23937  mdsymlem3  23946  mdsymlem5  23948  cdj3lem2b  23978  cdj3i  23982  supssd  24133  resspos  24222  resstos  24223  tpr2rico  24345  xrge0iifcnv  24354  ballotlemfc0  24785  ballotlemfcc  24786  subfacp1lem6  24906  iccllyscon  24972  cvmfolem  25001  cvmliftlem7  25013  cvmliftlem10  25016  ghomf1olem  25140  dedekind  25222  fprodss  25309  fundmpss  25425  dfon2lem3  25447  dfon2lem6  25450  axext4dist  25463  setlikess  25505  trpredtr  25543  trpredmintr  25544  dftrpred3g  25546  trpredrec  25551  frmin  25552  soseq  25564  wfrlem12  25584  frrlem5e  25625  frrlem11  25629  sltval2  25646  sltres  25654  nodenselem4  25674  nodenselem8  25678  nobndlem6  25687  dfrdg4  25830  brbtwn2  25879  colinearalg  25884  axcontlem10  25947  5segofs  25975  cgrextend  25977  segconeu  25980  btwncomim  25982  btwnswapid  25986  btwnintr  25988  btwnexch3  25989  btwndiff  25996  ifscgr  26013  cgrxfr  26024  btwnxfr  26025  lineext  26045  brofs2  26046  linecgr  26050  lineid  26052  idinside  26053  endofsegid  26054  btwnconn1lem13  26068  btwnconn3  26072  onsuct0  26226  limsucncmpi  26230  ltflcei  26275  tan2h  26280  heicant  26281  mblfinlem2  26284  mblfinlem3  26285  itg2addnclem  26298  itg2addnclem2  26299  itg2gt0cn  26302  ftc1anclem5  26326  ftc1anclem6  26327  finminlem  26363  nn0prpwlem  26367  cldbnd  26371  clsint2  26374  reftr  26411  fnessref  26415  comppfsc  26429  neibastop3  26433  fgmin  26441  filbcmb  26484  nninfnub  26497  mettrifi  26505  geomcau  26507  istotbnd3  26522  sstotbnd2  26525  ismtybndlem  26557  heibor1lem  26560  heiborlem1  26562  heiborlem8  26569  heiborlem10  26571  heibor  26572  riscer  26646  crngohomfo  26658  keridl  26684  ispridl2  26690  ispridlc  26722  fphpdo  26990  icodiamlt  26995  pellexlem5  27008  pellexlem6  27009  jm2.26lem3  27184  dfac21  27253  unxpwdom3  27345  ordpss  27742  stoweidlem34  27871  ltsubnn0  28218  elfz2z  28226  elfzmlbm  28227  elfzmlbp  28228  elfz0fzfz0  28235  ubmelm1fzo  28248  fzo1fzo0n0  28249  fzofzim  28257  wrdlenge2n0  28306  swrdnd  28314  swrdvalodmlem1  28319  swrdvalodm2  28320  swrdswrdlem  28330  swrdswrd  28331  swrdccatin12lem3a  28340  swrdccatin12lem3b  28341  swrdccatin12lem4  28345  swrdccat3a  28349  swrdccat3blem  28350  2cshw1lem1  28380  2cshw1lem2  28381  2cshwmod  28389  cshweqdif2s  28403  usg2wlkeq  28440  usgra2adedgspthlem2  28450  usg2wotspth  28514  usgravd00  28534  19.41rg  28809  dvelimvNEW7  29636  dral1NEW7  29667  cbv1hwAUX7  29685  sbiedNEW7  29714  sbequiNEW7  29753  ax7w15lemxAUX7  29840  cbv1hOLD7  29893  lsatcveq0  30004  eqlkr3  30073  atlatmstc  30291  atlrelat1  30293  hlrelat2  30374  intnatN  30378  cvrexchlem  30390  cvratlem  30392  cvrat2  30400  atltcvr  30406  cvrat3  30413  cvrat4  30414  ps-1  30448  ps-2  30449  lplnnle2at  30512  lvolnle3at  30553  2llnma3r  30759  cdlemblem  30764  pmapjoin  30823  elpcliN  30864  lhpmcvr4N  30997  4atexlemnclw  31041  trlnidatb  31148  cdlemc4  31165  cdlemd3  31171  cdleme3g  31205  cdleme7d  31217  cdleme11c  31232  cdleme11dN  31233  cdleme21b  31297  cdleme21c  31298  cdleme21i  31306  cdleme22b  31312  cdleme35fnpq  31420  cdlemf1  31532  trlord  31540  cdlemg6c  31591  dihglblem6  32312  dochlkr  32357  dochkrshp  32358  dihjat1lem  32400  dochexmidlem5  32436  dochexmidlem8  32439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator