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

Theorem syld 47
Description: Syllogism deduction. Deduction associated with syl 17. See conventions 27387 for the meaning of "associated deduction" or "deduction form". (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
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 25 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpdd 43 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syldc  48  3syld  60  sylsyld  61  nsyld  154  pm2.61d  170  sylibd  229  sylbid  230  sylibrd  249  sylbird  250  syland  497  ax12v2  2089  alrimdd  2121  axc16g  2172  axc16nf  2175  axc11rvOLD  2178  axc11r  2223  alrimddOLD  2231  nfeqf2  2333  sbequi  2403  2eu1  2582  axext3  2633  trel3  4793  poss  5066  sess2  5112  wefrc  5137  wereu2  5140  funun  5970  ssimaex  6302  f1cofveqaeq  6555  f1imass  6561  soisoi  6618  isores3  6625  isofrlem  6630  isoselem  6631  weniso  6644  abnexg  7006  oninton  7042  orduniorsuc  7072  limuni3  7094  tfindsg  7102  limom  7122  f1o2ndf1  7330  soxp  7335  extmptsuppeq  7364  smoel  7502  tfrlem9  7526  tz7.49  7585  seqomlem1  7590  odi  7704  omass  7705  omeulem2  7708  oeordsuc  7719  oeeulem  7726  ertr  7802  swoord2  7819  ecopovtrn  7893  domtriord  8147  onomeneq  8191  unxpdomlem2  8206  isinf  8214  pssnn  8219  findcard3  8244  frfi  8246  unblem3  8255  dffi3  8378  en3lplem1  8549  inf3lem5  8567  cantnfle  8606  cantnfp1lem3  8615  rankxpsuc  8783  tcrank  8785  ficardom  8825  carduni  8845  infxpenlem  8874  dfac8alem  8890  ac10ct  8895  ween  8896  alephdom  8942  alephle  8949  iscard3  8954  alephfp  8969  cdainf  9052  pwsdompw  9064  infdif  9069  cfslbn  9127  cofsmo  9129  cfcof  9134  fin1a2s  9274  domtriomlem  9302  ac6num  9339  zorn2lem3  9358  axdclem2  9380  imadomg  9394  iundom2g  9400  ficard  9425  fpwwe2lem8  9497  fpwwe2  9503  gchaclem  9538  tskr1om2  9628  inar1  9635  tskord  9640  tskuni  9643  grudomon  9677  grur1a  9679  grur1  9680  addnidpi  9761  ltexnq  9835  genpnnp  9865  addclprlem2  9877  mulclprlem  9879  psslinpr  9891  ltexprlem6  9901  ltexprlem7  9902  addcanpr  9906  mulgt0sr  9964  map2psrpr  9969  supsrlem  9970  axrrecex  10022  letr  10169  dedekind  10238  recex  10697  lemul12b  10918  mulgt1  10920  fimaxre2  11007  lbreu  11011  nnrecgt0  11096  nnunb  11326  bndndx  11329  zeo  11501  uzind  11507  fzind  11513  fnn0ind  11514  suprfinzcl  11530  suprzcl2  11816  zmax  11823  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  xrletr  12027  qbtwnre  12068  qsqueeze  12070  qextltlem  12071  xralrple  12074  xlesubadd  12131  supxrunb1  12187  icoshft  12332  zltaddlt1le  12362  fzen  12396  elfz0fzfz0  12483  elfzmlbp  12489  elfzo0z  12549  fzofzim  12554  fzo1fzo0n0  12558  elfzodifsumelfzo  12573  ssfzoulel  12602  modadd1  12747  modmul1  12763  uzrdgfni  12797  fsuppmapnn0fiub0  12833  fsuppmapnn0ub  12835  fsuppmapnn0fz  12836  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  seqsplit  12874  seqf1olem1  12880  seqf1olem2  12881  seqid2  12887  seqhomo  12888  expnbnd  13033  faclbnd4lem4  13123  seqcoll  13286  hashle2pr  13297  elss2prb  13307  ccatalpha  13411  swrdsbslen  13494  swrdspsleq  13495  swrdswrdlem  13505  swrdswrd  13506  reuccats1lem  13525  swrdccatin12lem2a  13531  swrdccatin12lem2b  13532  swrdccatin12lem3  13536  swrdccat3a  13540  swrdccat3blem  13541  repswswrd  13577  cshf1  13602  swrd2lsw  13741  sqeqd  13950  sqrmo  14036  cau3lem  14138  icodiamlt  14218  limsupbnd2  14258  lo1bdd2  14299  climuni  14327  rlimcn2  14365  mulcn2  14370  o1of2  14387  rlimo1  14391  lo1le  14426  isercolllem1  14439  iseralt  14459  cvgrat  14659  fprodss  14722  znnenlem  14984  rpnnen2lem12  14998  ruclem3  15006  sqrt2irr  15023  p1modz1  15034  dvdsmodexp  15035  dvds2lem  15041  dvdslelem  15078  dvdsabseq  15082  divalglem8  15170  bitsinv1lem  15210  sadcaddlem  15226  smu01lem  15254  smueqlem  15259  bezoutlem4  15306  dfgcd2  15310  algcvga  15339  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfdvdsb  15403  coprmgcdb  15409  coprmdvds2  15415  coprmprod  15422  isprm3  15443  prmdvdsfz  15464  isprm5  15466  coprm  15470  rpexp12i  15481  phibndlem  15522  dfphi2  15526  eulerthlem2  15534  odzdvds  15547  iserodd  15587  pclem  15590  pcpremul  15595  pcqcl  15608  pcdvdsb  15620  pcprmpw2  15633  difsqpwdvds  15638  pcaddlem  15639  pcmptcl  15642  pcfac  15650  prmpwdvds  15655  unbenlem  15659  prmreclem1  15667  4sqlem17  15712  vdwmc2  15730  vdwlem9  15740  vdwlem10  15741  vdwlem13  15744  vdwnnlem3  15748  ramcl  15780  prmgaplem7  15808  mreiincl  16303  initoid  16702  termoid  16703  initoeu2lem1  16711  pospo  17020  dirge  17284  gsmsymgrfixlem1  17893  oddvdsnn0  18009  oddvds  18012  odcl2  18028  gexdvds  18045  sylow1lem1  18059  sylow2alem2  18079  sylow2a  18080  efgi2  18184  efgsrel  18193  efgs1b  18195  cyggex2  18344  telgsums  18436  pgpfac1lem2  18520  pgpfac1lem3a  18521  pgpfac1lem3  18522  pgpfac1lem5  18524  lmodfopnelem2  18948  lssssr  19001  cply1mul  19712  gsummoncoe1  19722  gzrngunitlem  19859  znunit  19960  frgpcyg  19970  lsmcss  20084  obselocv  20120  obslbs  20122  cpmatacl  20569  cpmatinvcl  20570  cpmatmcllem  20571  m2cpminvid2lem  20607  mp2pm2mplem4  20662  pm2mp  20678  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmul0  20711  chfacfpmmul0  20715  cayhamlem4  20741  ordtrest2lem  21055  leordtval2  21064  lecldbas  21071  cncls  21126  cncnp  21132  cnpresti  21140  lmcnp  21156  cnt0  21198  isreg2  21229  cmpsublem  21250  cmpsub  21251  tgcmp  21252  bwth  21261  dfconn2  21270  1stcfb  21296  1stcelcls  21312  islly2  21335  dislly  21348  reftr  21365  comppfsc  21383  kgencn2  21408  txcnp  21471  txindis  21485  txcmplem1  21492  txlm  21499  xkohaus  21504  cnmptcom  21529  kqfvima  21581  isr0  21588  fgss2  21725  fbasrn  21735  filuni  21736  ufilmax  21758  isufil2  21759  cfinufil  21779  fmfnfmlem1  21805  fmfnfmlem2  21806  fmfnfmlem4  21808  fmfnfm  21809  fmco  21812  flimopn  21826  hausflim  21832  flimrest  21834  fclsopn  21865  flimfnfcls  21879  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALT  21902  ptcmplem2  21904  cnextcn  21918  symgtgp  21952  qustgplem  21971  tsmsres  21994  tsmsxplem1  22003  isucn2  22130  imasdsf1olem  22225  bldisj  22250  blssps  22276  blss  22277  metcnp3  22392  ngptgp  22487  nrginvrcn  22543  nmoleub  22582  xrsmopn  22662  icccmplem3  22674  reconnlem2  22677  rectbntr0  22682  rescncf  22747  iocopnst  22786  iccpnfcnv  22790  lebnumii  22812  nmoleub2lem  22960  nmhmcn  22966  iscfil3  23117  iscau2  23121  iscau3  23122  iscau4  23123  iscmet3lem2  23136  cfilres  23140  caussi  23141  equivcfil  23143  equivcau  23144  ivthlem2  23267  ivthlem3  23268  ovoliunlem2  23317  ovoliunnul  23321  ovolicc2lem3  23333  ioombl1lem4  23375  dyadmax  23412  dyadmbl  23414  volsup2  23419  itg2le  23551  itg2const2  23553  itg2seq  23554  itgsplitioo  23649  dvnres  23739  rolle  23798  c1lip1  23805  dvivthlem1  23816  lhop1  23822  dvcnvrelem1  23825  dvfsumrlim  23839  ply1divmo  23940  ig1peu  23976  plypf1  24013  coeaddlem  24050  fta1  24108  quotcan  24109  aalioulem4  24135  ulmcaulem  24193  ulmcn  24198  pilem2  24251  sincosq1lem  24294  sinq12gt0  24304  sinq12ge0  24305  tanord1  24328  lognegb  24381  logrec  24546  dcubic  24618  xrlimcnp  24740  o1cxp  24746  ftalem2  24845  ftalem3  24846  fsumdvdscom  24956  chtub  24982  vmasum  24986  bcmono  25047  bposlem3  25056  bposlem7  25060  lgsdir  25102  lgsqrlem2  25117  lgsqrmodndvds  25123  lgsdchr  25125  gausslemma2dlem6  25142  gausslemma2d  25144  lgsquadlem2  25151  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  2sqlem6  25193  dchrisumlem3  25225  pntrsumbnd2  25301  pntpbnd1  25320  pntibnd  25327  pntlem3  25343  pntleml  25345  brbtwn2  25830  colinearalg  25835  axcontlem10  25898  edgupgr  26074  edglnl  26083  usgruspgrb  26121  subupgr  26224  uhgrspan1  26240  usgredgsscusgredg  26411  fusgrn0degnn0  26451  upgrewlkle2  26558  uspgr2wlkeq  26598  redwlk  26625  wlkdlem2  26636  upgrwlkdvdelem  26688  pthdlem1  26718  pthdlem2  26720  crctcshwlkn0lem3  26760  wlkiswwlks1  26821  wwlksm1edg  26835  wwlksnred  26855  wwlksnextbi  26857  umgr2adedgspth  26913  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a  26964  clwwisshclwwslemlem  26970  clwwlkf  27010  clwwlkext2edg  27020  wwlksubclwwlk  27023  clwwlknonwwlknonbOLD  27081  clwwlknonex2lem2  27083  eupth2lems  27216  frgrwopreglem4a  27290  frgrregorufrg  27306  ex-natded5.3-2  27395  isgrpo  27479  vacn  27677  ubthlem2  27855  htthlem  27902  normgt0  28112  shmodsi  28376  spansneleq  28557  h1datomi  28568  nmcexi  29013  pjnormssi  29155  stm1add3i  29234  golem2  29259  cvnsym  29277  dmdmd  29287  mdslmd1lem1  29312  mdslmd1i  29316  mdexchi  29322  atcveq0  29335  superpos  29341  hatomistici  29349  atoml2i  29370  atcvat2i  29374  chirredlem1  29377  atcvat3i  29383  mdsymlem3  29392  mdsymlem5  29394  cdj3lem2b  29424  cdj3i  29428  supssd  29615  infssd  29616  2sqmod  29776  resspos  29787  resstos  29788  submarchi  29868  tpr2rico  30086  ordtrest2NEWlem  30096  xrge0iifcnv  30107  omssubadd  30490  eulerpartlemb  30558  ballotlemfc0  30682  ballotlemfcc  30683  ftc2re  30804  subfacp1lem6  31293  iccllysconn  31358  cvmfolem  31387  cvmliftlem7  31399  cvmliftlem10  31402  fundmpss  31790  dfon2lem3  31814  dfon2lem6  31817  axext4dist  31830  trpredtr  31854  trpredmintr  31855  dftrpred3g  31857  trpredrec  31862  frpomin  31863  frmin  31867  soseq  31879  frrlem5e  31913  sltres  31940  nosepon  31943  nolesgn2o  31949  nodenselem8  31966  nosupbnd1lem1  31979  dfrdg4  32183  5segofs  32238  cgrextend  32240  segconeu  32243  btwncomim  32245  btwnswapid  32249  btwnintr  32251  btwnexch3  32252  btwndiff  32259  ifscgr  32276  cgrxfr  32287  btwnxfr  32288  lineext  32308  brofs2  32309  linecgr  32313  lineid  32315  idinside  32316  endofsegid  32317  btwnconn1lem13  32331  btwnconn3  32335  finminlem  32437  nn0prpwlem  32442  cldbnd  32446  clsint2  32449  fnessref  32477  neibastop3  32482  fgmin  32490  onsuct0  32565  limsucncmpi  32569  bj-axc14  32964  bj-restn0  33168  bj-0int  33180  wl-19.2reqv  33440  wl-aetr  33447  fin2so  33526  tan2h  33531  lindsenlbs  33534  poimirlem2  33541  poimirlem9  33548  poimirlem17  33556  poimirlem18  33557  poimirlem21  33560  poimirlem23  33562  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimir  33572  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  itg2addnclem  33591  itg2addnclem2  33592  itg2gt0cn  33595  ftc1anclem5  33619  ftc1anclem6  33620  filbcmb  33665  nninfnub  33677  mettrifi  33683  geomcau  33685  istotbnd3  33700  sstotbnd2  33703  ismtybndlem  33735  heibor1lem  33738  heiborlem1  33740  heiborlem8  33747  heiborlem10  33749  heibor  33750  opidonOLD  33781  riscer  33917  crngohomfo  33935  keridl  33961  ispridl2  33967  ispridlc  33999  ac6s6  34110  dral1-o  34508  ax12indalem  34549  ax12inda2ALT  34550  lsatcveq0  34637  eqlkr3  34706  atlatmstc  34924  atlrelat1  34926  hlrelat2  35007  intnatN  35011  cvrexchlem  35023  cvratlem  35025  cvrat2  35033  atltcvr  35039  cvrat3  35046  cvrat4  35047  ps-1  35081  ps-2  35082  lplnnle2at  35145  lvolnle3at  35186  2llnma3r  35392  cdlemblem  35397  pmapjoin  35456  elpcliN  35497  lhpmcvr4N  35630  4atexlemnclw  35674  trlnidatb  35782  cdlemc4  35799  cdlemd3  35805  cdleme3g  35839  cdleme7d  35851  cdleme11c  35866  cdleme11dN  35867  cdleme21b  35931  cdleme21c  35932  cdleme21i  35940  cdleme22b  35946  cdleme35fnpq  36054  cdlemf1  36166  trlord  36174  cdlemg6c  36225  dihglblem6  36946  dochlkr  36991  dochkrshp  36992  dihjat1lem  37034  dochexmidlem5  37070  dochexmidlem8  37073  fphpdo  37698  pellexlem5  37714  pellexlem6  37715  jm2.26lem3  37885  unxpwdom3  37982  ov2ssiunov2  38309  frege124d  38370  ordpss  38972  19.41rg  39083  monoordxrv  40025  stoweidlem34  40569  ralralimp  41619  zm1nn  41641  elfz2z  41650  smonoord  41666  iccpartlt  41685  iccelpart  41694  icceuelpartlem  41696  fargshiftf1  41702  pfxccatin12lem1  41748  reuccatpfxs1lem  41758  goldbachthlem2  41783  odz2prm2pw  41800  fmtnoprmfac1lem  41801  fmtnofac2lem  41805  prmdvdsfmtnof1  41824  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem4  41852  gbegt5  41974  gbowge7  41976  bgoldbtbndlem4  42021  bgoldbtbnd  42022  tgoldbach  42030  tgoldbachOLD  42037  sprsymrelf1lem  42066  zrtermorngc  42326  zrtermoringc  42395  lcosslsp  42552  lindslinindsimp1  42571  snlindsntor  42585  m1modmmod  42641  setrec1lem4  42762  aacllem  42875
  Copyright terms: Public domain W3C validator