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  1794  cbv1hOLD  1990  dveeq2  2021  ax10o2  2037  dvelimvOLD  2041  dral1OLD  2074  equveli  2101  sbequi  2127  sbequiOLD  2131  sbiedOLD  2168  dral1-o  2272  ax11indalem  2314  ax11inda2ALT  2315  trel3  4394  poss  4597  sess2  4643  wefrc  4668  wereu2  4671  ordelord  4695  oninton  4872  orduniorsuc  4902  limuni3  4924  tfindsg  4932  limom  4952  funun  5594  ssimaex  5888  f1dmex  6071  f1imass  6110  soisoi  6148  isores3  6155  isofrlem  6160  isoselem  6161  weniso  6175  f1o2ndf1  6558  soxp  6563  smoel  6717  smogt  6724  tfrlem9  6741  tz7.49  6797  seqomlem1  6802  abianfp  6811  odi  6917  omass  6918  omeulem2  6921  oeordsuc  6932  oeeulem  6939  ertr  7015  swoord2  7030  ecopovtrn  7102  domtriord  7348  2pwuninel  7357  onomeneq  7391  unxpdomlem2  7409  isinf  7417  pssnn  7422  findcard3  7445  frfi  7447  unblem3  7456  dffi3  7531  inf3lem3  7680  inf3lem5  7682  noinfep  7709  cantnfle  7721  cantnfp1lem3  7731  en3lplem1  7765  rankxpsuc  7903  tcrank  7905  ficardom  7945  carduni  7965  infxpenlem  7992  dfac8alem  8007  ac10ct  8012  ween  8013  alephdom  8059  alephle  8066  iscard3  8071  alephfp  8086  cdainf  8169  pwsdompw  8181  infdif  8186  cfslbn  8244  cofsmo  8246  cfsmolem  8247  cfcof  8251  fin1a2s  8391  domtriomlem  8419  ac6num  8456  zorn2lem3  8475  axdclem2  8497  imadomg  8509  iundom2g  8512  ficard  8537  fpwwe2lem8  8609  fpwwe2  8615  gchaclem  8650  tskr1om2  8740  inar1  8747  tskord  8752  tskuni  8755  grudomon  8789  grur1a  8791  grur1  8792  addnidpi  8875  ltexnq  8949  genpnnp  8979  addclprlem2  8991  mulclprlem  8993  psslinpr  9005  ltaddpr2  9009  ltexprlem6  9015  ltexprlem7  9016  addcanpr  9020  mulgt0sr  9077  map2psrpr  9082  supsrlem  9083  axrrecex  9135  letr  9265  recex  9752  lemul12b  9965  mulgt1  9967  ledivmulOLD  9982  fimaxre2  10054  lbreu  10056  nnrecgt0  10135  nnunb  10315  bndndx  10318  zeo  10453  uzind  10459  fzind  10466  fnn0ind  10467  lbzbi  10664  suprzcl2  10666  zmax  10671  rpnnen1lem5  10704  xrletr  10848  qbtwnre  10885  qsqueeze  10887  qextltlem  10888  xralrple  10891  xlesubadd  10942  supxrunb1  10998  icoshft  11119  fzen  11172  modadd1  11381  modmul1  11383  uzrdgfni  11402  seqcl2  11445  seqfveq2  11449  seqshft2  11453  monoord  11457  seqsplit  11460  seqf1olem1  11466  seqf1olem2  11467  seqid2  11473  seqhomo  11474  expnbnd  11612  faclbnd4lem4  11691  seqcoll  11816  sqeqd  12091  sqrmo  12177  cau3lem  12278  limsupbnd2  12397  lo1bdd2  12438  climuni  12466  rlimcn2  12504  mulcn2  12509  o1of2  12526  rlimo1  12530  lo1le  12565  isercolllem1  12578  iseralt  12598  isumrpcl  12743  cvgrat  12780  rpnnen2  12945  ruclem3  12952  sqr2irr  12968  dvds2lem  12982  dvdslelem  13014  divalglem8  13040  bitsinv1lem  13073  sadcaddlem  13089  smu01lem  13117  smueqlem  13122  bezoutlem4  13161  algcvga  13190  isprm3  13208  coprm  13220  coprmdvds2  13223  isprm5  13232  rpexp12i  13242  phibndlem  13279  dfphi2  13283  eulerthlem2  13291  odzdvds  13301  iserodd  13329  pclem  13332  pcpremul  13337  pcqcl  13350  pcdvdsb  13362  pcprmpw2  13375  pcaddlem  13377  pcmptcl  13380  pcfac  13388  prmpwdvds  13392  unbenlem  13396  prmreclem1  13404  4sqlem17  13449  vdwmc2  13467  vdwlem9  13477  vdwlem10  13478  vdwlem13  13481  vdwnnlem3  13485  ramcl  13517  mreiincl  13941  pospo  14550  dirge  14814  oddvdsnn0  15314  oddvds  15317  odcl2  15333  gexdvds  15350  sylow1lem1  15364  sylow2alem2  15384  sylow2a  15385  efgi2  15489  efgsrel  15498  efgs1b  15500  cyggex2  15638  pgpfac1lem2  15765  pgpfac1lem3a  15766  pgpfac1lem3  15767  pgpfac1lem5  15769  lssssr  16161  gzrngunitlem  16895  znunit  16976  frgpcyg  16986  lsmcss  17051  obselocv  17087  obslbs  17089  ordtrest2lem  17399  leordtval2  17408  lecldbas  17415  cncls  17470  cncnp  17476  cnpresti  17484  lmcnp  17500  cnt0  17542  isreg2  17573  cmpsublem  17594  cmpsub  17595  tgcmp  17596  bwth  17605  dfcon2  17614  1stcfb  17640  2ndcctbss  17650  1stcelcls  17656  islly2  17679  dislly  17692  kgencn2  17721  txcnp  17784  txindis  17798  txcmplem1  17805  txlm  17812  xkohaus  17817  cnmptcom  17842  kqfvima  17894  isr0  17901  fgss2  18038  fbasrn  18048  filuni  18049  ufilmax  18071  isufil2  18072  cfinufil  18092  fmfnfmlem1  18118  fmfnfmlem2  18119  fmfnfmlem4  18121  fmfnfm  18122  fmco  18125  flimopn  18139  hausflim  18145  flimrest  18147  fclsopn  18178  flimfnfcls  18192  alexsubALTlem2  18211  alexsubALTlem3  18212  alexsubALT  18214  ptcmplem2  18216  cnextcn  18230  symgtgp  18263  divstgplem  18282  tsmsres  18305  tsmsxplem1  18314  isucn2  18441  imasdsf1olem  18535  bldisj  18560  blssps  18586  blss  18587  metcnp3  18702  ngptgp  18809  nrginvrcn  18859  nmoleub  18897  xrsmopn  18975  icccmplem3  18987  reconnlem2  18990  rectbntr0  18995  rescncf  19059  icoopnst  19096  iocopnst  19097  iccpnfcnv  19101  lebnumii  19123  nmoleub2lem  19254  nmhmcn  19260  fgcfil  19356  iscfil3  19358  iscau2  19362  iscau3  19363  iscau4  19364  iscmet3lem2  19377  cfilres  19381  caussi  19382  equivcfil  19384  equivcau  19385  caubl  19392  ivthlem2  19481  ivthlem3  19482  ovoliunlem2  19531  ovoliunnul  19535  ovolicc2lem3  19547  ioombl1lem4  19587  dyadmax  19622  dyadmbl  19624  volsup2  19629  itg2le  19761  itg2const2  19763  itg2seq  19764  itgsplitioo  19859  dvnres  19949  rolle  20006  c1lip1  20013  dvivthlem1  20024  lhop1  20030  dvcnvrelem1  20033  dvfsumrlim  20047  ply1divmo  20190  ig1peu  20226  plypf1  20263  coeaddlem  20299  fta1  20357  quotcan  20358  aalioulem4  20384  ulmcaulem  20442  ulmcn  20447  pilem2  20500  sincosq1lem  20537  sinq12gt0  20547  sinq12ge0  20548  sineq0  20561  tanord1  20571  lognegb  20616  logrec  20793  dcubic  20818  xrlimcnp  20939  o1cxp  20945  ftalem2  20988  ftalem3  20989  fsumdvdscom  21102  chtub  21128  vmasum  21132  bcmono  21193  bposlem3  21202  bposlem7  21206  lgsdir  21246  lgsqrlem2  21258  lgsdchr  21264  lgsquadlem2  21271  2sqlem6  21285  dchrisumlem3  21317  pntrsumbnd2  21393  pntpbnd1  21412  pntibnd  21419  pntlem3  21435  pntleml  21437  redwlk  21738  fargshiftf1  21756  constr3trllem2  21770  4cycl4dv  21786  vdusgra0nedg  21811  usgravd0nedg  21815  eupath2  21834  ex-natded5.3-2  21848  isgrpo  21916  opidon  22042  vacn  22322  ubthlem2  22505  htthlem  22552  normgt0  22761  shmodsi  23023  spansneleq  23204  h1datomi  23215  pjjsi  23334  nmcexi  23661  pjnormssi  23803  stm1add3i  23882  golem2  23907  cvnsym  23925  dmdmd  23935  mdslmd1lem1  23960  mdslmd1i  23964  mdexchi  23970  atcveq0  23983  superpos  23989  hatomistici  23997  atoml2i  24018  atcvat2i  24022  chirredlem1  24025  atcvat3i  24031  mdsymlem3  24040  mdsymlem5  24042  cdj3lem2b  24072  cdj3i  24076  supssd  24249  resspos  24369  resstos  24370  submarchi  24453  tpr2rico  24639  ordtrest2NEWlem  24649  xrge0iifcnv  24660  eulerpartlemb  25043  ballotlemfc0  25143  ballotlemfcc  25144  subfacp1lem6  25337  iccllyscon  25403  cvmfolem  25432  cvmliftlem7  25444  cvmliftlem10  25447  ghomf1olem  25571  dedekind  25644  fprodss  25731  fundmpss  25847  dfon2lem3  25869  dfon2lem6  25872  axext4dist  25885  setlikess  25927  trpredtr  25965  trpredmintr  25966  dftrpred3g  25968  trpredrec  25973  frmin  25974  soseq  25986  wfrlem12  26006  frrlem5e  26047  frrlem11  26051  sltval2  26068  sltres  26076  nodenselem4  26096  nodenselem8  26100  nobndlem6  26109  dfrdg4  26252  brbtwn2  26301  colinearalg  26306  axcontlem10  26369  5segofs  26397  cgrextend  26399  segconeu  26402  btwncomim  26404  btwnswapid  26408  btwnintr  26410  btwnexch3  26411  btwndiff  26418  ifscgr  26435  cgrxfr  26446  btwnxfr  26447  lineext  26467  brofs2  26468  linecgr  26472  lineid  26474  idinside  26475  endofsegid  26476  btwnconn1lem13  26490  btwnconn3  26494  onsuct0  26648  limsucncmpi  26652  ltflcei  26689  tan2h  26694  heicant  26695  mblfinlem2  26698  mblfinlem3  26699  itg2addnclem  26712  itg2addnclem2  26713  itg2gt0cn  26716  ftc1anclem5  26740  ftc1anclem6  26741  finminlem  26777  nn0prpwlem  26781  cldbnd  26785  clsint2  26788  reftr  26825  fnessref  26829  comppfsc  26843  neibastop3  26847  fgmin  26855  filbcmb  26898  nninfnub  26911  mettrifi  26919  geomcau  26921  istotbnd3  26936  sstotbnd2  26939  ismtybndlem  26971  heibor1lem  26974  heiborlem1  26976  heiborlem8  26983  heiborlem10  26985  heibor  26986  riscer  27060  crngohomfo  27072  keridl  27098  ispridl2  27104  ispridlc  27136  fphpdo  27400  icodiamlt  27405  pellexlem5  27418  pellexlem6  27419  jm2.26lem3  27594  dfac21  27663  unxpwdom3  27755  ordpss  28150  stoweidlem34  28277  ralralimp  28575  ltsubnn0  28644  elfz2z  28667  elfzmlbm  28668  elfzmlbp  28669  elfz0fzfz0  28676  ubmelm1fzo  28695  fzo1fzo0n0  28696  fzofzim  28703  elfzo0z  28712  swrdnd  28830  swrdvalodmlem1  28835  swrdvalodm2  28836  swrdswrdlem  28848  swrdswrd  28849  swrd2ls  28857  swrdccatin12lem3a  28871  swrdccatin12lem3b  28872  swrdccatin12lem4  28876  swrdccat3a  28880  swrdccat3blem  28881  ccat2s1fvw  28902  2cshw1lem1  28920  2cshw1lem2  28921  2cshwmod  28929  cshweqdif2s  28936  usg2wlkeq  28973  usgra2adedgspthlem2  28988  wwlknred  29039  wwlknextbi  29041  wwlkm1edg  29051  usg2wotspth  29087  clwlkswlks  29107  clwlkisclwwlklem2fv2  29129  clwlkisclwwlklem2a  29131  clwlkisclwwlklem1  29133  clwwlkf  29140  clwwlkext2edg  29148  wwlksubclwwlk  29150  clwwisshclwwlem1b  29156  zm1nn  29161  clwwisshclwwlem3  29164  usgravd00  29233  frgraregorufrg  29360  numclwwlkovf2ex  29374  numclwlk1lem2foa  29379  numclwlk1lem2fo  29383  19.41rg  29603  dvelimvNEW7  30512  dral1NEW7  30543  cbv1hwAUX7  30561  sbiedNEW7  30590  sbequiNEW7  30629  ax7w15lemxAUX7  30716  cbv1hOLD7  30769  lsatcveq0  30879  eqlkr3  30948  atlatmstc  31166  atlrelat1  31168  hlrelat2  31249  intnatN  31253  cvrexchlem  31265  cvratlem  31267  cvrat2  31275  atltcvr  31281  cvrat3  31288  cvrat4  31289  ps-1  31323  ps-2  31324  lplnnle2at  31387  lvolnle3at  31428  2llnma3r  31634  cdlemblem  31639  pmapjoin  31698  elpcliN  31739  lhpmcvr4N  31872  4atexlemnclw  31916  trlnidatb  32023  cdlemc4  32040  cdlemd3  32046  cdleme3g  32080  cdleme7d  32092  cdleme11c  32107  cdleme11dN  32108  cdleme21b  32172  cdleme21c  32173  cdleme21i  32181  cdleme22b  32187  cdleme35fnpq  32295  cdlemf1  32407  trlord  32415  cdlemg6c  32466  dihglblem6  33187  dochlkr  33232  dochkrshp  33233  dihjat1lem  33275  dochexmidlem5  33311  dochexmidlem8  33314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator