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 28106 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  159  pm2.61d  180  sylibd  240  sylbid  241  sylibrd  260  sylbird  261  syland  602  animpimp2impd  840  ax12v2  2169  alrimdd  2204  axc16g  2251  axc16nf  2254  axc11r  2377  sb1OLD  2500  sb4a  2502  sbequiOLD  2527  sbequiALT  2589  2eu1  2728  2eu1OLD  2729  2eu1v  2730  ss2ralv  4032  ss2rexv  4033  trel3  5171  poss  5469  sess2  5517  wefrc  5542  wereu2  5545  funun  6393  ssimaex  6741  f1cofveqaeq  7007  f1imass  7013  soisoi  7070  isores3  7077  isofrlem  7082  isoselem  7083  weniso  7096  abnexg  7467  oninton  7504  orduniorsuc  7534  limuni3  7556  tfindsg  7564  limom  7584  f1o2ndf1  7807  soxp  7812  extmptsuppeq  7843  smoel  7986  tfrlem9  8010  tz7.49  8070  seqomlem1  8075  odi  8194  omass  8195  omeulem2  8198  oeordsuc  8209  oeeulem  8216  ertr  8293  swoord2  8310  ecopovtrn  8389  domtriord  8651  onomeneq  8696  unxpdomlem2  8711  isinf  8719  pssnn  8724  findcard3  8749  frfi  8751  unblem3  8760  en3lplem1  9063  inf3lem5  9083  cantnfle  9122  cantnfp1lem3  9131  rankxpsuc  9299  tcrank  9301  ficardom  9378  carduni  9398  infxpenlem  9427  dfac8alem  9443  ac10ct  9448  ween  9449  alephdom  9495  alephle  9502  iscard3  9507  alephfp  9522  pwsdompw  9614  infdif  9619  cfslbn  9677  cofsmo  9679  cfcof  9684  fin1a2s  9824  domtriomlem  9852  ac6num  9889  zorn2lem3  9908  axdclem2  9930  imadomg  9944  iundom2g  9950  ficard  9975  fpwwe2lem8  10047  fpwwe2  10053  gchpwdom  10080  gchaclem  10088  tskr1om2  10178  inar1  10185  tskord  10190  tskuni  10193  grudomon  10227  grur1a  10229  grur1  10230  addnidpi  10311  ltexnq  10385  genpnnp  10415  addclprlem2  10427  mulclprlem  10429  psslinpr  10441  ltexprlem6  10451  ltexprlem7  10452  addcanpr  10456  mulgt0sr  10515  map2psrpr  10520  supsrlem  10521  axrrecex  10573  letr  10722  dedekind  10791  recex  11260  lemul12b  11485  mulgt1  11487  fimaxre2  11574  lbreu  11579  nnrecgt0  11668  nnunb  11881  bndndx  11884  zeo  12056  uzind  12062  fzind  12068  fnn0ind  12069  suprfinzcl  12085  suprzcl2  12326  zmax  12333  rpnnen1lem5  12368  xrletr  12539  qbtwnre  12580  qsqueeze  12582  qextltlem  12583  xralrple  12586  xlesubadd  12644  supxrunb1  12700  icoshft  12847  zltaddlt1le  12878  fzen  12912  elfz0fzfz0  13000  elfzmlbp  13006  elfzo0z  13067  fzofzim  13072  fzo1fzo0n0  13076  elfzodifsumelfzo  13091  ssfzoulel  13119  modadd1  13264  modmul1  13280  uzrdgfni  13314  fsuppmapnn0fiub0  13349  fsuppmapnn0ub  13351  fsuppmapnn0fz  13352  seqf1olem1  13397  seqf1olem2  13398  expnbnd  13581  faclbnd4lem4  13644  hashgt23el  13773  seqcoll  13810  hashle2pr  13823  elss2prb  13833  ccatalpha  13935  swrdsbslen  14014  swrdspsleq  14015  swrdswrdlem  14054  swrdswrd  14055  pfxccatin12lem2a  14077  pfxccatin12lem1  14078  pfxccatin12lem3  14082  swrdccat3blem  14089  reuccatpfxs1lem  14096  repswswrd  14134  cshf1  14160  swrd2lsw  14302  sqeqd  14513  sqrmo  14599  cau3lem  14702  icodiamlt  14783  limsupbnd2  14828  lo1bdd2  14869  climuni  14897  rlimcn2  14935  mulcn2  14940  o1of2  14957  rlimo1  14961  lo1le  14996  iseralt  15029  cvgrat  15227  fprodss  15290  rpnnen2lem12  15566  ruclem3  15574  sqrt2irr  15590  p1modz1  15602  dvdsmodexp  15603  dvds2lem  15610  dvdslelem  15647  dvdsabseq  15651  divalglem8  15739  bitsinv1lem  15778  sadcaddlem  15794  smu01lem  15822  smueqlem  15827  bezoutlem4  15878  dfgcd2  15882  algcvga  15911  lcmfunsnlem1  15969  lcmfunsnlem2lem1  15970  lcmfunsnlem2lem2  15971  lcmfdvdsb  15975  coprmgcdb  15981  coprmdvds2  15986  coprmprod  15993  isprm3  16015  prmdvdsfz  16037  isprm5  16039  coprm  16043  rpexp12i  16054  phibndlem  16095  dfphi2  16099  eulerthlem2  16107  odzdvds  16120  iserodd  16160  pclem  16163  pcpremul  16168  pcqcl  16181  pcdvdsb  16193  pcprmpw2  16206  difsqpwdvds  16211  pcaddlem  16212  pcmptcl  16215  pcfac  16223  prmpwdvds  16228  unbenlem  16232  prmreclem1  16240  4sqlem17  16285  vdwmc2  16303  vdwlem9  16313  vdwlem10  16314  vdwlem13  16317  vdwnnlem3  16321  ramcl  16353  prmgaplem7  16381  mreiincl  16855  initoid  17253  termoid  17254  initoeu2lem1  17262  pospo  17571  dirge  17835  cyccom  18284  gsmsymgrfixlem1  18484  oddvdsnn0  18601  oddvds  18604  odcl2  18621  gexdvds  18638  sylow2alem2  18672  sylow2a  18673  efgi2  18780  efgsrel  18789  efgs1b  18791  cyggex2  18946  telgsums  19042  pgpfac1lem2  19126  pgpfac1lem3a  19127  pgpfac1lem3  19128  pgpfac1lem5  19130  lmodfopnelem2  19600  lssssr  19654  cply1mul  20390  gsummoncoe1  20400  gzrngunitlem  20538  znunit  20638  frgpcyg  20648  lsmcss  20764  obselocv  20800  obslbs  20802  cpmatacl  21252  cpmatinvcl  21253  cpmatmcllem  21254  m2cpminvid2lem  21290  mp2pm2mplem4  21345  pm2mp  21361  chfacfisf  21390  chfacfisfcpmat  21391  chfacfscmul0  21394  chfacfpmmul0  21398  cayhamlem4  21424  ordtrest2lem  21739  leordtval2  21748  lecldbas  21755  cncls  21810  cncnp  21816  cnpresti  21824  lmcnp  21840  cnt0  21882  isreg2  21913  cmpsublem  21935  cmpsub  21936  tgcmp  21937  bwth  21946  dfconn2  21955  1stcfb  21981  1stcelcls  21997  islly2  22020  dislly  22033  reftr  22050  comppfsc  22068  kgencn2  22093  txcnp  22156  txindis  22170  txcmplem1  22177  txlm  22184  xkohaus  22189  cnmptcom  22214  kqfvima  22266  isr0  22273  fgss2  22410  fbasrn  22420  filuni  22421  ufilmax  22443  isufil2  22444  cfinufil  22464  fmfnfmlem1  22490  fmfnfmlem2  22491  fmfnfmlem4  22493  fmfnfm  22494  fmco  22497  flimopn  22511  hausflim  22517  flimrest  22519  fclsopn  22550  flimfnfcls  22564  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALT  22587  ptcmplem2  22589  cnextcn  22603  symgtgp  22637  qustgplem  22656  tsmsres  22679  tsmsxplem1  22688  isucn2  22815  imasdsf1olem  22910  bldisj  22935  blssps  22961  blss  22962  metcnp3  23077  ngptgp  23172  nrginvrcn  23228  nmoleub  23267  xrsmopn  23347  icccmplem3  23359  reconnlem2  23362  rectbntr0  23367  rescncf  23432  iocopnst  23471  iccpnfcnv  23475  lebnumii  23497  nmoleub2lem  23645  nmhmcn  23651  iscfil3  23803  iscau2  23807  iscau3  23808  iscau4  23809  iscmet3lem2  23822  caussi  23827  equivcfil  23829  equivcau  23830  ivthlem2  23980  ivthlem3  23981  ovoliunlem2  24031  ovoliunnul  24035  ioombl1lem4  24089  dyadmax  24126  dyadmbl  24128  volsup2  24133  itg2le  24267  itg2const2  24269  itg2seq  24270  itgsplitioo  24365  rolle  24514  c1lip1  24521  dvivthlem1  24532  lhop1  24538  dvcnvrelem1  24541  dvfsumrlim  24555  ply1divmo  24656  ig1peu  24692  plypf1  24729  coeaddlem  24766  fta1  24824  quotcan  24825  aalioulem4  24851  ulmcaulem  24909  ulmcn  24914  pilem2  24967  sincosq1lem  25010  sinq12gt0  25020  sinq12ge0  25021  tanord1  25048  lognegb  25100  logrec  25268  logbgcd1irr  25299  dcubic  25351  xrlimcnp  25473  o1cxp  25479  ftalem2  25578  ftalem3  25579  fsumdvdscom  25689  chtub  25715  vmasum  25719  bcmono  25780  bposlem3  25789  bposlem7  25793  lgsdir  25835  lgsqrlem2  25850  lgsqrmodndvds  25856  gausslemma2dlem6  25875  gausslemma2d  25877  lgsquadlem2  25884  2lgslem3a1  25903  2lgslem3b1  25904  2lgslem3c1  25905  2lgslem3d1  25906  2sqlem6  25926  2sq2  25936  2sqmod  25939  dchrisumlem3  25994  pntrsumbnd2  26070  pntpbnd1  26089  pntibnd  26096  pntlem3  26112  pntleml  26114  brbtwn2  26618  colinearalg  26623  axcontlem10  26686  edgupgr  26846  edglnl  26855  usgruspgrb  26893  subupgr  26996  uhgrspan1  27012  usgredgsscusgredg  27168  fusgrn0degnn0  27208  upgrewlkle2  27315  uspgr2wlkeq  27354  redwlk  27381  wlkdlem2  27392  upgrwlkdvdelem  27444  pthdlem1  27474  pthdlem2  27476  crctcshwlkn0lem3  27517  wlkiswwlks1  27572  wwlksm1edg  27586  wwlksnred  27597  wwlksnextbi  27599  umgr2adedgspth  27654  clwlkclwwlklem2fv2  27701  clwlkclwwlklem2a  27703  clwlkclwwlkf1lem3  27711  clwwisshclwwslemlem  27718  clwwlkf  27753  clwwlkext2edg  27762  wwlksubclwwlk  27764  clwwlknonex2lem2  27814  eupth2lems  27944  frgrwopreglem4a  28016  frgrregorufrg  28032  ex-natded5.3-2  28114  isgrpo  28201  vacn  28398  ubthlem2  28575  htthlem  28621  normgt0  28831  shmodsi  29093  spansneleq  29274  h1datomi  29285  nmcexi  29730  pjnormssi  29872  stm1add3i  29951  golem2  29976  cvnsym  29994  dmdmd  30004  mdslmd1lem1  30029  mdslmd1i  30033  mdexchi  30039  atcveq0  30052  superpos  30058  hatomistici  30066  atoml2i  30087  atcvat2i  30091  chirredlem1  30094  atcvat3i  30100  mdsymlem3  30109  mdsymlem5  30111  cdj3lem2b  30141  cdj3i  30145  supssd  30371  infssd  30372  resspos  30573  resstos  30574  submarchi  30742  tpr2rico  31054  ordtrest2NEWlem  31064  xrge0iifcnv  31075  omssubadd  31457  eulerpartlemb  31525  ballotlemfc0  31649  ballotlemfcc  31650  ftc2re  31768  loop1cycl  32281  subfacp1lem6  32329  iccllysconn  32394  cvmfolem  32423  satfsschain  32508  satfrel  32511  satfdm  32513  sat1el2xp  32523  satffunlem1lem1  32546  dmopab3rexdif  32549  satffunlem2lem2  32550  satffun  32553  fundmpss  32906  dfon2lem3  32927  dfon2lem6  32930  axextbdist  32942  trpredtr  32966  trpredmintr  32967  dftrpred3g  32969  trpredrec  32974  frpomin  32975  frmin  32981  soseq  32993  sltres  33066  nosepon  33069  nolesgn2o  33075  nodenselem8  33092  nosupbnd1lem1  33105  dfrdg4  33309  5segofs  33364  cgrextend  33366  segconeu  33369  btwncomim  33371  btwnswapid  33375  btwnintr  33377  btwnexch3  33378  btwndiff  33385  ifscgr  33402  cgrxfr  33413  btwnxfr  33414  lineext  33434  brofs2  33435  linecgr  33439  lineid  33441  idinside  33442  endofsegid  33443  btwnconn1lem13  33457  btwnconn3  33461  finminlem  33563  nn0prpwlem  33567  cldbnd  33571  clsint2  33574  fnessref  33602  neibastop3  33607  fgmin  33615  onsuct0  33686  limsucncmpi  33690  bj-nnfea  33961  bj-axc14  34077  bj-restn0  34275  bj-0int  34287  wl-19.2reqv  34646  wl-aetr  34651  fin2so  34760  tan2h  34765  lindsenlbs  34768  poimirlem2  34775  poimirlem9  34782  poimirlem17  34790  poimirlem18  34791  poimirlem21  34794  poimirlem23  34796  poimirlem26  34799  poimirlem29  34802  poimirlem30  34803  poimirlem31  34804  poimir  34806  heicant  34808  mblfinlem2  34811  mblfinlem3  34812  itg2addnclem  34824  itg2addnclem2  34825  itg2gt0cn  34828  ftc1anclem5  34852  ftc1anclem6  34853  filbcmb  34896  nninfnub  34907  mettrifi  34913  geomcau  34915  istotbnd3  34930  sstotbnd2  34933  ismtybndlem  34965  heibor1lem  34968  heiborlem1  34970  heiborlem8  34977  heiborlem10  34979  heibor  34980  opidonOLD  35011  riscer  35147  crngohomfo  35165  keridl  35191  ispridl2  35197  ispridlc  35229  ac6s6  35331  eqvreltr  35722  dral1-o  35920  ax12indalem  35961  ax12inda2ALT  35962  lsatcveq0  36048  eqlkr3  36117  atlatmstc  36335  atlrelat1  36337  hlrelat2  36419  intnatN  36423  cvrexchlem  36435  cvratlem  36437  cvrat2  36445  atltcvr  36451  cvrat3  36458  cvrat4  36459  ps-1  36493  ps-2  36494  lplnnle2at  36557  lvolnle3at  36598  2llnma3r  36804  cdlemblem  36809  pmapjoin  36868  elpcliN  36909  lhpmcvr4N  37042  4atexlemnclw  37086  trlnidatb  37193  cdlemc4  37210  cdlemd3  37216  cdleme3g  37250  cdleme7d  37262  cdleme11c  37277  cdleme11dN  37278  cdleme21b  37342  cdleme21c  37343  cdleme21i  37351  cdleme22b  37357  cdleme35fnpq  37465  cdlemf1  37577  trlord  37585  cdlemg6c  37636  dihglblem6  38356  dochlkr  38401  dochkrshp  38402  dihjat1lem  38444  dochexmidlem5  38480  dochexmidlem8  38483  qsalrel  39003  remulcand  39128  fphpdo  39292  pellexlem5  39308  pellexlem6  39309  jm2.26lem3  39476  unxpwdom3  39573  iscard5  39779  ov2ssiunov2  39923  frege124d  39984  ordpss  40660  19.41rg  40761  stoweidlem34  42196  euoreqb  43185  2reu8i  43189  ralralimp  43354  f1oresf1o2  43367  zm1nn  43379  elfz2z  43392  iccpartlt  43461  iccelpart  43470  icceuelpartlem  43472  fargshiftf1  43478  sprsymrelf1lem  43530  paireqne  43550  reuopreuprim  43565  goldbachthlem2  43585  odz2prm2pw  43602  fmtnoprmfac1lem  43603  fmtnofac2lem  43607  prmdvdsfmtnof1  43626  sfprmdvdsmersenne  43645  lighneallem2  43648  lighneallem4  43652  fppr2odd  43773  gbegt5  43803  gbowge7  43805  bgoldbtbndlem4  43850  bgoldbtbnd  43851  tgoldbach  43859  isomuspgrlem2b  43871  isomgrsym  43878  zrtermorngc  44200  zrtermoringc  44269  lcosslsp  44421  lindslinindsimp1  44440  snlindsntor  44454  m1modmmod  44509  eenglngeehlnmlem2  44653  itsclc0yqsol  44679  itschlc0xyqsol1  44681  itschlc0xyqsol  44682  setrec1lem4  44721  aacllem  44830
  Copyright terms: Public domain W3C validator