Theorem syld 46

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 26650 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

Step	Hyp	Ref	Expression
1		syld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syld.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	2	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpdd 42	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  3syld  58  sylsyld  59  nsyld  153  pm2.61d  169  sylibd  228  sylbid  229  sylibrd  248  sylbird  249  syland  497  ax12v2  2036  ax12vOLD  2037  ax12vOLDOLD  2038  alrimdd  2070  axc16g  2119  axc16nf  2122  axc11rvOLD  2125  axc11r  2175  alrimddOLD  2183  nfeqf2  2285  sbequi  2363  2eu1  2541  axext3  2592  trel3  4688  poss  4961  sess2  5007  wefrc  5032  wereu2  5035  funun  5846  ssimaex  6173  f1imass  6422  soisoi  6478  isores3  6485  isofrlem  6490  isoselem  6491  weniso  6504  oninton  6892  orduniorsuc  6922  limuni3  6944  tfindsg  6952  limom  6972  f1o2ndf1  7172  soxp  7177  extmptsuppeq  7206  wfrlem12  7313  smoel  7344  smogt  7351  tfrlem9  7368  tz7.49  7427  seqomlem1  7432  odi  7546  omass  7547  omeulem2  7550  oeordsuc  7561  oeeulem  7568  ertr  7644  swoord2  7661  ecopovtrn  7737  domtriord  7991  onomeneq  8035  unxpdomlem2  8050  isinf  8058  pssnn  8063  findcard3  8088  frfi  8090  unblem3  8099  dffi3  8220  en3lplem1  8394  inf3lem3  8410  inf3lem5  8412  noinfep  8440  cantnfle  8451  cantnfp1lem3  8460  rankxpsuc  8628  tcrank  8630  ficardom  8670  carduni  8690  infxpenlem  8719  dfac8alem  8735  ac10ct  8740  ween  8741  alephdom  8787  alephle  8794  iscard3  8799  alephfp  8814  cdainf  8897  pwsdompw  8909  infdif  8914  cfslbn  8972  cofsmo  8974  cfsmolem  8975  cfcof  8979  fin1a2s  9119  domtriomlem  9147  ac6num  9184  zorn2lem3  9203  axdclem2  9225  imadomg  9237  iundom2g  9241  ficard  9266  fpwwe2lem8  9338  fpwwe2  9344  gchaclem  9379  tskr1om2  9469  inar1  9476  tskord  9481  tskuni  9484  grudomon  9518  grur1a  9520  grur1  9521  addnidpi  9602  ltexnq  9676  genpnnp  9706  addclprlem2  9718  mulclprlem  9720  psslinpr  9732  ltaddpr2  9736  ltexprlem6  9742  ltexprlem7  9743  addcanpr  9747  mulgt0sr  9805  map2psrpr  9810  supsrlem  9811  axrrecex  9863  letr  10010  dedekind  10079  recex  10538  lemul12b  10759  mulgt1  10761  fimaxre2  10848  lbreu  10852  nnrecgt0  10935  nnunb  11165  bndndx  11168  zeo  11339  uzind  11345  fzind  11351  fnn0ind  11352  suprfinzcl  11368  suprzcl2  11654  zmax  11661  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  xrletr  11865  qbtwnre  11904  qsqueeze  11906  qextltlem  11907  xralrple  11910  xlesubadd  11965  supxrunb1  12021  icoshft  12165  zltaddlt1le  12195  fzen  12229  elfz1b  12279  elfz0fzfz0  12313  elfzmlbp  12319  elfzo0z  12377  fzofzim  12382  fzo1fzo0n0  12386  elfzodifsumelfzo  12401  ssfzoulel  12428  modadd1  12569  modmul1  12585  uzrdgfni  12619  fsuppmapnn0fiub0  12655  fsuppmapnn0ub  12657  fsuppmapnn0fz  12658  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqf1olem1  12702  seqf1olem2  12703  seqid2  12709  seqhomo  12710  expnbnd  12855  faclbnd4lem4  12945  seqcoll  13105  elss2prb  13123  fundmge2nop0  13129  ccatalpha  13228  swrdsbslen  13300  swrdspsleq  13301  swrdswrdlem  13311  swrdswrd  13312  reuccats1lem  13331  swrdccatin12lem2a  13336  swrdccatin12lem2b  13337  swrdccatin12lem3  13341  swrdccat3a  13345  swrdccat3blem  13346  repswswrd  13382  cshf1  13407  swrd2lsw  13543  sqeqd  13754  sqrmo  13840  cau3lem  13942  icodiamlt  14022  limsupbnd2  14062  lo1bdd2  14103  climuni  14131  rlimcn2  14169  mulcn2  14174  o1of2  14191  rlimo1  14195  lo1le  14230  isercolllem1  14243  iseralt  14263  cvgrat  14454  fprodss  14517  znnenlem  14779  rpnnen2lem12  14793  ruclem3  14801  sqrt2irr  14817  dvds2lem  14832  dvdslelem  14869  dvdsabseq  14873  divalglem8  14961  bitsinv1lem  15001  sadcaddlem  15017  smu01lem  15045  smueqlem  15050  bezoutlem4  15097  dfgcd2  15101  algcvga  15130  lcmf  15184  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfdvdsb  15194  coprmgcdb  15200  coprmdvds2  15206  coprmprod  15213  isprm3  15234  prmdvdsfz  15255  isprm5  15257  coprm  15261  rpexp12i  15272  ncoprmlnprm  15274  phibndlem  15313  dfphi2  15317  eulerthlem2  15325  odzdvds  15338  iserodd  15378  pclem  15381  pcpremul  15386  pcqcl  15399  pcdvdsb  15411  pcprmpw2  15424  difsqpwdvds  15429  pcaddlem  15430  pcmptcl  15433  pcfac  15441  prmpwdvds  15446  unbenlem  15450  prmreclem1  15458  4sqlem17  15503  vdwmc2  15521  vdwlem9  15531  vdwlem10  15532  vdwlem13  15535  vdwnnlem3  15539  ramcl  15571  prmgaplem7  15599  mreiincl  16079  initoid  16478  termoid  16479  initoeu1  16484  initoeu2lem1  16487  termoeu1  16491  pospo  16796  dirge  17060  dfgrp3lem  17336  gsmsymgrfixlem1  17670  oddvdsnn0  17786  oddvds  17789  odcl2  17805  gexdvds  17822  sylow1lem1  17836  sylow2alem2  17856  sylow2a  17857  efgi2  17961  efgsrel  17970  efgs1b  17972  cyggex2  18121  telgsums  18213  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfac1lem5  18301  lmodfopnelem2  18723  lssssr  18774  cply1mul  19485  gsummoncoe1  19495  gzrngunitlem  19630  znunit  19731  frgpcyg  19741  lsmcss  19855  obselocv  19891  obslbs  19893  scmataddcl  20141  scmatsubcl  20142  cpmatacl  20340  cpmatinvcl  20341  cpmatmcllem  20342  m2cpminvid2lem  20378  mp2pm2mplem4  20433  pm2mp  20449  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmul0  20482  chfacfpmmul0  20486  cayhamlem4  20512  ordtrest2lem  20817  leordtval2  20826  lecldbas  20833  cncls  20888  cncnp  20894  cnpresti  20902  lmcnp  20918  cnt0  20960  isreg2  20991  cmpsublem  21012  cmpsub  21013  tgcmp  21014  bwth  21023  dfcon2  21032  1stcfb  21058  2ndcctbss  21068  1stcelcls  21074  islly2  21097  dislly  21110  reftr  21127  comppfsc  21145  kgencn2  21170  txcnp  21233  txindis  21247  txcmplem1  21254  txlm  21261  xkohaus  21266  cnmptcom  21291  kqfvima  21343  isr0  21350  fgss2  21488  fbasrn  21498  filuni  21499  ufilmax  21521  isufil2  21522  cfinufil  21542  fmfnfmlem1  21568  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  fmco  21575  flimopn  21589  hausflim  21595  flimrest  21597  fclsopn  21628  flimfnfcls  21642  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALT  21665  ptcmplem2  21667  cnextcn  21681  symgtgp  21715  qustgplem  21734  tsmsres  21757  tsmsxplem1  21766  isucn2  21893  imasdsf1olem  21988  bldisj  22013  blssps  22039  blss  22040  metcnp3  22155  ngptgp  22250  nrginvrcn  22306  nmoleub  22345  xrsmopn  22423  icccmplem3  22435  reconnlem2  22438  rectbntr0  22443  rescncf  22508  iocopnst  22547  iccpnfcnv  22551  lebnumii  22573  nmoleub2lem  22722  nmhmcn  22728  fgcfil  22877  iscfil3  22879  iscau2  22883  iscau3  22884  iscau4  22885  iscmet3lem2  22898  cfilres  22902  caussi  22903  equivcfil  22905  equivcau  22906  ivthlem2  23028  ivthlem3  23029  ovoliunlem2  23078  ovoliunnul  23082  ovolicc2lem3  23094  ioombl1lem4  23136  dyadmax  23172  dyadmbl  23174  volsup2  23179  itg2le  23312  itg2const2  23314  itg2seq  23315  itgsplitioo  23410  dvnres  23500  rolle  23557  c1lip1  23564  dvivthlem1  23575  lhop1  23581  dvcnvrelem1  23584  dvfsumrlim  23598  ply1divmo  23699  ig1peu  23735  plypf1  23772  coeaddlem  23809  fta1  23867  quotcan  23868  aalioulem4  23894  ulmcaulem  23952  ulmcn  23957  pilem2  24010  sincosq1lem  24053  sinq12gt0  24063  sinq12ge0  24064  tanord1  24087  lognegb  24140  logrec  24301  dcubic  24373  xrlimcnp  24495  o1cxp  24501  ftalem2  24600  ftalem3  24601  fsumdvdscom  24711  chtub  24737  vmasum  24741  bcmono  24802  bposlem3  24811  bposlem7  24815  lgsdir  24857  lgsqrlem2  24872  lgsqrmodndvds  24878  lgsdchr  24880  gausslemma2dlem6  24897  gausslemma2d  24899  lgsquadlem2  24906  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  2sqlem6  24948  dchrisumlem3  24980  pntrsumbnd2  25056  pntpbnd1  25075  pntibnd  25082  pntlem3  25098  pntleml  25100  brbtwn2  25585  colinearalg  25590  axcontlem10  25653  edgupgr  25808  upgredg  25811  redwlk  26136  usgra2adedgspthlem2  26140  fargshiftf1  26165  constr3trllem2  26179  4cycl4dv  26195  usg2wlkeq  26236  wwlknred  26251  wwlknextbi  26253  wwlkm1edg  26263  clwlkswlks  26286  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkf  26322  clwwlkext2edg  26330  wwlksubclwwlk  26332  clwwisshclwwlem1  26333  usg2wotspth  26411  vdusgra0nedg  26435  usgravd0nedg  26445  usgravd00  26446  eupath2  26507  frgraregorufrg  26599  numclwwlkovf2ex  26613  numclwlk1lem2foa  26618  numclwlk1lem2fo  26622  ex-natded5.3-2  26657  isgrpo  26735  vacn  26933  ubthlem2  27111  htthlem  27158  normgt0  27368  shmodsi  27632  spansneleq  27813  h1datomi  27824  pjjsi  27943  nmcexi  28269  pjnormssi  28411  stm1add3i  28490  golem2  28515  cvnsym  28533  dmdmd  28543  mdslmd1lem1  28568  mdslmd1i  28572  mdexchi  28578  atcveq0  28591  superpos  28597  hatomistici  28605  atoml2i  28626  atcvat2i  28630  chirredlem1  28633  atcvat3i  28639  mdsymlem3  28648  mdsymlem5  28650  cdj3lem2b  28680  cdj3i  28684  supssd  28870  infssd  28871  2sqmod  28979  resspos  28990  resstos  28991  submarchi  29071  tpr2rico  29286  ordtrest2NEWlem  29296  xrge0iifcnv  29307  omssubadd  29689  eulerpartlemb  29757  ballotlemfc0  29881  ballotlemfcc  29882  subfacp1lem6  30421  iccllyscon  30486  cvmfolem  30515  cvmliftlem7  30527  cvmliftlem10  30530  fundmpss  30910  dfon2lem3  30934  dfon2lem6  30937  axext4dist  30950  trpredtr  30974  trpredmintr  30975  dftrpred3g  30977  trpredrec  30982  frmin  30983  soseq  30995  frrlem5e  31032  frrlem11  31036  sltval2  31053  sltres  31061  nosepon  31066  nodenselem4  31083  nodenselem8  31087  nobndlem6  31096  dfrdg4  31228  5segofs  31283  cgrextend  31285  segconeu  31288  btwncomim  31290  btwnswapid  31294  btwnintr  31296  btwnexch3  31297  btwndiff  31304  ifscgr  31321  cgrxfr  31332  btwnxfr  31333  lineext  31353  brofs2  31354  linecgr  31358  lineid  31360  idinside  31361  endofsegid  31362  btwnconn1lem13  31376  btwnconn3  31380  finminlem  31482  nn0prpwlem  31487  cldbnd  31491  clsint2  31494  fnessref  31522  neibastop3  31527  fgmin  31535  onsuct0  31610  limsucncmpi  31614  bj-exalimi  31801  bj-axc14  32032  bj-restn0  32224  wl-19.2reqv  32489  wl-dveeq12  32490  wl-aetr  32496  fin2so  32566  tan2h  32571  lindsenlbs  32574  poimirlem2  32581  poimirlem9  32588  poimirlem17  32596  poimirlem18  32597  poimirlem21  32600  poimirlem23  32602  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimir  32612  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  itg2addnclem  32631  itg2addnclem2  32632  itg2gt0cn  32635  ftc1anclem5  32659  ftc1anclem6  32660  filbcmb  32705  nninfnub  32717  mettrifi  32723  geomcau  32725  istotbnd3  32740  sstotbnd2  32743  ismtybndlem  32775  heibor1lem  32778  heiborlem1  32780  heiborlem8  32787  heiborlem10  32789  heibor  32790  opidonOLD  32821  riscer  32957  crngohomfo  32975  keridl  33001  ispridl2  33007  ispridlc  33039  ac6s6  33150  dral1-o  33207  ax12indalem  33248  ax12inda2ALT  33249  lsatcveq0  33337  eqlkr3  33406  atlatmstc  33624  atlrelat1  33626  hlrelat2  33707  intnatN  33711  cvrexchlem  33723  cvratlem  33725  cvrat2  33733  atltcvr  33739  cvrat3  33746  cvrat4  33747  ps-1  33781  ps-2  33782  lplnnle2at  33845  lvolnle3at  33886  2llnma3r  34092  cdlemblem  34097  pmapjoin  34156  elpcliN  34197  lhpmcvr4N  34330  4atexlemnclw  34374  trlnidatb  34482  cdlemc4  34499  cdlemd3  34505  cdleme3g  34539  cdleme7d  34551  cdleme11c  34566  cdleme11dN  34567  cdleme21b  34632  cdleme21c  34633  cdleme21i  34641  cdleme22b  34647  cdleme35fnpq  34755  cdlemf1  34867  trlord  34875  cdlemg6c  34926  dihglblem6  35647  dochlkr  35692  dochkrshp  35693  dihjat1lem  35735  dochexmidlem5  35771  dochexmidlem8  35774  fphpdo  36399  pellexlem5  36415  pellexlem6  36416  jm2.26lem3  36586  dfac21  36654  unxpwdom3  36683  ov2ssiunov2  37011  frege124d  37072  ordpss  37676  19.41rg  37787  stoweidlem34  38927  smonoord  39944  iccpartlt  39962  iccelpart  39971  icceuelpartlem  39973  goldbachthlem2  39996  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnofac2lem  40018  prmdvdsfmtnof1  40037  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem4  40065  gbegt5  40183  gboge7  40185  nnsum3primesle9  40210  evengpop3  40214  evengpoap3  40215  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239  pfxccatin12lem1  40286  reuccatpfxs1lem  40296  ralralimp  40309  f1cofveqaeq  40323  zm1nn  40348  elfz2z  40352  usgruspgrb  40411  subupgr  40511  uhgrspan1  40527  usgredgsscusgredg  40675  fusgrn0degnn0  40714  upgrewlkle2  40808  uspgr2wlkeq  40854  red1wlk  40881  1wlkdlem2  40892  upgrwlkdvdelem  40942  pthdlem1  40972  pthdlem2  40974  crctcsh1wlkn0lem3  41015  0enwwlksnge1  41060  1wlkiswwlks1  41064  wwlksm1edg  41078  wwlksnred  41098  wwlksnextbi  41100  umgr2adedgspth  41155  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksf  41222  clwwlksext2edg  41230  wwlksubclwwlks  41232  clwwisshclwwslemlem  41233  clwlksfclwwlk  41269  conngrv2edg  41362  eupth2lems  41406  frgrregorufrg  41505  av-numclwwlkovf2ex  41517  av-numclwlk1lem2foa  41521  av-numclwlk1lem2fo  41525  zrtermorngc  41793  zrtermoringc  41862  ztprmneprm  41918  lcosslsp  42021  lindslinindsimp1  42040  lindslinindsimp2lem5  42045  snlindsntor  42054  m1modmmod  42110  flnn0div2ge  42121  setrec1lem4  42236  aacllem  42356