Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 27871 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 43	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:  syldc  48  3syld  60  sylsyld  61  nsyld  159  pm2.61d  180  sylibd  240  sylbid  241  sylibrd  260  sylbird  261  syland  602  animpimp2impd  841  ax12v2  2143  alrimdd  2179  axc16g  2224  axc16nf  2227  axc11r  2343  sb1  2461  sb4a  2463  sbequiOLD  2488  sbequiALT  2550  2eu1  2705  2eu1OLD  2706  2eu1v  2707  ss2ralv  3956  ss2rexv  3957  trel3  5071  poss  5364  sess2  5412  wefrc  5437  wereu2  5440  funun  6270  ssimaex  6615  f1cofveqaeq  6881  f1imass  6887  soisoi  6944  isores3  6951  isofrlem  6956  isoselem  6957  weniso  6970  abnexg  7335  oninton  7371  orduniorsuc  7401  limuni3  7423  tfindsg  7431  limom  7451  f1o2ndf1  7671  soxp  7676  extmptsuppeq  7705  smoel  7849  tfrlem9  7873  tz7.49  7932  seqomlem1  7937  odi  8055  omass  8056  omeulem2  8059  oeordsuc  8070  oeeulem  8077  ertr  8154  swoord2  8171  ecopovtrn  8250  domtriord  8510  onomeneq  8554  unxpdomlem2  8569  isinf  8577  pssnn  8582  findcard3  8607  frfi  8609  unblem3  8618  en3lplem1  8921  inf3lem5  8941  cantnfle  8980  cantnfp1lem3  8989  rankxpsuc  9157  tcrank  9159  ficardom  9236  carduni  9256  infxpenlem  9285  dfac8alem  9301  ac10ct  9306  ween  9307  alephdom  9353  alephle  9360  iscard3  9365  alephfp  9380  pwsdompw  9472  infdif  9477  cfslbn  9535  cofsmo  9537  cfcof  9542  fin1a2s  9682  domtriomlem  9710  ac6num  9747  zorn2lem3  9766  axdclem2  9788  imadomg  9802  iundom2g  9808  ficard  9833  fpwwe2lem8  9905  fpwwe2  9911  gchpwdom  9938  gchaclem  9946  tskr1om2  10036  inar1  10043  tskord  10048  tskuni  10051  grudomon  10085  grur1a  10087  grur1  10088  addnidpi  10169  ltexnq  10243  genpnnp  10273  addclprlem2  10285  mulclprlem  10287  psslinpr  10299  ltexprlem6  10309  ltexprlem7  10310  addcanpr  10314  mulgt0sr  10373  map2psrpr  10378  supsrlem  10379  axrrecex  10431  letr  10581  dedekind  10650  recex  11120  lemul12b  11345  mulgt1  11347  fimaxre2  11434  lbreu  11439  nnrecgt0  11528  nnunb  11741  bndndx  11744  zeo  11917  uzind  11923  fzind  11929  fnn0ind  11930  suprfinzcl  11946  suprzcl2  12187  zmax  12194  rpnnen1lem5  12230  xrletr  12401  qbtwnre  12442  qsqueeze  12444  qextltlem  12445  xralrple  12448  xlesubadd  12506  supxrunb1  12562  icoshft  12709  zltaddlt1le  12740  fzen  12774  elfz0fzfz0  12862  elfzmlbp  12868  elfzo0z  12929  fzofzim  12934  fzo1fzo0n0  12938  elfzodifsumelfzo  12953  ssfzoulel  12981  modadd1  13126  modmul1  13142  uzrdgfni  13176  fsuppmapnn0fiub0  13211  fsuppmapnn0ub  13213  fsuppmapnn0fz  13214  seqf1olem1  13259  seqf1olem2  13260  expnbnd  13443  faclbnd4lem4  13506  hashgt23el  13633  seqcoll  13670  hashle2pr  13681  elss2prb  13691  ccatalpha  13791  swrdsbslen  13862  swrdspsleq  13863  swrdswrdlem  13902  swrdswrd  13903  pfxccatin12lem2a  13925  pfxccatin12lem1  13926  pfxccatin12lem3  13930  swrdccat3blem  13937  reuccatpfxs1lem  13944  repswswrd  13982  cshf1  14008  swrd2lsw  14150  sqeqd  14359  sqrmo  14445  cau3lem  14548  icodiamlt  14629  limsupbnd2  14674  lo1bdd2  14715  climuni  14743  rlimcn2  14781  mulcn2  14786  o1of2  14803  rlimo1  14807  lo1le  14842  iseralt  14875  cvgrat  15072  fprodss  15135  rpnnen2lem12  15411  ruclem3  15419  sqrt2irr  15435  p1modz1  15447  dvdsmodexp  15448  dvds2lem  15455  dvdslelem  15492  dvdsabseq  15496  divalglem8  15584  bitsinv1lem  15623  sadcaddlem  15639  smu01lem  15667  smueqlem  15672  bezoutlem4  15719  dfgcd2  15723  algcvga  15752  lcmfunsnlem1  15810  lcmfunsnlem2lem1  15811  lcmfunsnlem2lem2  15812  lcmfdvdsb  15816  coprmgcdb  15822  coprmdvds2  15827  coprmprod  15834  isprm3  15856  prmdvdsfz  15878  isprm5  15880  coprm  15884  rpexp12i  15895  phibndlem  15936  dfphi2  15940  eulerthlem2  15948  odzdvds  15961  iserodd  16001  pclem  16004  pcpremul  16009  pcqcl  16022  pcdvdsb  16034  pcprmpw2  16047  difsqpwdvds  16052  pcaddlem  16053  pcmptcl  16056  pcfac  16064  prmpwdvds  16069  unbenlem  16073  prmreclem1  16081  4sqlem17  16126  vdwmc2  16144  vdwlem9  16154  vdwlem10  16155  vdwlem13  16158  vdwnnlem3  16162  ramcl  16194  prmgaplem7  16222  mreiincl  16696  initoid  17094  termoid  17095  initoeu2lem1  17103  pospo  17412  dirge  17676  gsmsymgrfixlem1  18286  oddvdsnn0  18403  oddvds  18406  odcl2  18422  gexdvds  18439  sylow2alem2  18473  sylow2a  18474  efgi2  18578  efgsrel  18587  efgs1b  18589  cyggex2  18738  telgsums  18830  pgpfac1lem2  18914  pgpfac1lem3a  18915  pgpfac1lem3  18916  pgpfac1lem5  18918  lmodfopnelem2  19361  lssssr  19415  cply1mul  20145  gsummoncoe1  20155  gzrngunitlem  20292  znunit  20392  frgpcyg  20402  lsmcss  20518  obselocv  20554  obslbs  20556  cpmatacl  21008  cpmatinvcl  21009  cpmatmcllem  21010  m2cpminvid2lem  21046  mp2pm2mplem4  21101  pm2mp  21117  chfacfisf  21146  chfacfisfcpmat  21147  chfacfscmul0  21150  chfacfpmmul0  21154  cayhamlem4  21180  ordtrest2lem  21495  leordtval2  21504  lecldbas  21511  cncls  21566  cncnp  21572  cnpresti  21580  lmcnp  21596  cnt0  21638  isreg2  21669  cmpsublem  21691  cmpsub  21692  tgcmp  21693  bwth  21702  dfconn2  21711  1stcfb  21737  1stcelcls  21753  islly2  21776  dislly  21789  reftr  21806  comppfsc  21824  kgencn2  21849  txcnp  21912  txindis  21926  txcmplem1  21933  txlm  21940  xkohaus  21945  cnmptcom  21970  kqfvima  22022  isr0  22029  fgss2  22166  fbasrn  22176  filuni  22177  ufilmax  22199  isufil2  22200  cfinufil  22220  fmfnfmlem1  22246  fmfnfmlem2  22247  fmfnfmlem4  22249  fmfnfm  22250  fmco  22253  flimopn  22267  hausflim  22273  flimrest  22275  fclsopn  22306  flimfnfcls  22320  alexsubALTlem2  22340  alexsubALTlem3  22341  alexsubALT  22343  ptcmplem2  22345  cnextcn  22359  symgtgp  22393  qustgplem  22412  tsmsres  22435  tsmsxplem1  22444  isucn2  22571  imasdsf1olem  22666  bldisj  22691  blssps  22717  blss  22718  metcnp3  22833  ngptgp  22928  nrginvrcn  22984  nmoleub  23023  xrsmopn  23103  icccmplem3  23115  reconnlem2  23118  rectbntr0  23123  rescncf  23188  iocopnst  23227  iccpnfcnv  23231  lebnumii  23253  nmoleub2lem  23401  nmhmcn  23407  iscfil3  23559  iscau2  23563  iscau3  23564  iscau4  23565  iscmet3lem2  23578  caussi  23583  equivcfil  23585  equivcau  23586  ivthlem2  23736  ivthlem3  23737  ovoliunlem2  23787  ovoliunnul  23791  ioombl1lem4  23845  dyadmax  23882  dyadmbl  23884  volsup2  23889  itg2le  24023  itg2const2  24025  itg2seq  24026  itgsplitioo  24121  rolle  24270  c1lip1  24277  dvivthlem1  24288  lhop1  24294  dvcnvrelem1  24297  dvfsumrlim  24311  ply1divmo  24412  ig1peu  24448  plypf1  24485  coeaddlem  24522  fta1  24580  quotcan  24581  aalioulem4  24607  ulmcaulem  24665  ulmcn  24670  pilem2  24723  sincosq1lem  24766  sinq12gt0  24776  sinq12ge0  24777  tanord1  24802  lognegb  24854  logrec  25022  logbgcd1irr  25053  dcubic  25105  xrlimcnp  25228  o1cxp  25234  ftalem2  25333  ftalem3  25334  fsumdvdscom  25444  chtub  25470  vmasum  25474  bcmono  25535  bposlem3  25544  bposlem7  25548  lgsdir  25590  lgsqrlem2  25605  lgsqrmodndvds  25611  gausslemma2dlem6  25630  gausslemma2d  25632  lgsquadlem2  25639  2lgslem3a1  25658  2lgslem3b1  25659  2lgslem3c1  25660  2lgslem3d1  25661  2sqlem6  25681  2sq2  25691  2sqmod  25694  dchrisumlem3  25749  pntrsumbnd2  25825  pntpbnd1  25844  pntibnd  25851  pntlem3  25867  pntleml  25869  brbtwn2  26374  colinearalg  26379  axcontlem10  26442  edgupgr  26602  edglnl  26611  usgruspgrb  26649  subupgr  26752  uhgrspan1  26768  usgredgsscusgredg  26924  fusgrn0degnn0  26964  upgrewlkle2  27071  uspgr2wlkeq  27110  redwlk  27139  wlkdlem2  27150  upgrwlkdvdelem  27204  pthdlem1  27234  pthdlem2  27236  crctcshwlkn0lem3  27277  wlkiswwlks1  27332  wwlksm1edg  27346  wwlksnred  27357  wwlksnextbi  27359  umgr2adedgspth  27414  clwlkclwwlklem2fv2  27461  clwlkclwwlklem2a  27463  clwlkclwwlkf1lem3  27471  clwwisshclwwslemlem  27478  clwwlkf  27513  clwwlkext2edg  27522  wwlksubclwwlk  27524  clwwlknonex2lem2  27574  eupth2lems  27705  frgrwopreglem4a  27781  frgrregorufrg  27797  ex-natded5.3-2  27879  isgrpo  27965  vacn  28162  ubthlem2  28339  htthlem  28385  normgt0  28595  shmodsi  28857  spansneleq  29038  h1datomi  29049  nmcexi  29494  pjnormssi  29636  stm1add3i  29715  golem2  29740  cvnsym  29758  dmdmd  29768  mdslmd1lem1  29793  mdslmd1i  29797  mdexchi  29803  atcveq0  29816  superpos  29822  hatomistici  29830  atoml2i  29851  atcvat2i  29855  chirredlem1  29858  atcvat3i  29864  mdsymlem3  29873  mdsymlem5  29875  cdj3lem2b  29905  cdj3i  29909  supssd  30133  infssd  30134  resspos  30320  resstos  30321  submarchi  30453  tpr2rico  30772  ordtrest2NEWlem  30782  xrge0iifcnv  30793  omssubadd  31175  eulerpartlemb  31243  ballotlemfc0  31367  ballotlemfcc  31368  ftc2re  31486  loop1cycl  31992  subfacp1lem6  32040  iccllysconn  32105  cvmfolem  32134  satfsschain  32219  satfrel  32222  satfdm  32224  sat1el2xp  32234  satffunlem1lem1  32257  dmopab3rexdif  32260  satffunlem2lem2  32261  satffun  32264  fundmpss  32617  dfon2lem3  32638  dfon2lem6  32641  axextbdist  32654  trpredtr  32678  trpredmintr  32679  dftrpred3g  32681  trpredrec  32686  frpomin  32687  frmin  32693  soseq  32705  sltres  32778  nosepon  32781  nolesgn2o  32787  nodenselem8  32804  nosupbnd1lem1  32817  dfrdg4  33021  5segofs  33076  cgrextend  33078  segconeu  33081  btwncomim  33083  btwnswapid  33087  btwnintr  33089  btwnexch3  33090  btwndiff  33097  ifscgr  33114  cgrxfr  33125  btwnxfr  33126  lineext  33146  brofs2  33147  linecgr  33151  lineid  33153  idinside  33154  endofsegid  33155  btwnconn1lem13  33169  btwnconn3  33173  finminlem  33275  nn0prpwlem  33279  cldbnd  33283  clsint2  33286  fnessref  33314  neibastop3  33319  fgmin  33327  onsuct0  33398  limsucncmpi  33402  bj-axc14  33750  bj-nnfea  33850  bj-restn0  33980  bj-0int  33992  wl-19.2reqv  34297  wl-aetr  34302  fin2so  34410  tan2h  34415  lindsenlbs  34418  poimirlem2  34425  poimirlem9  34432  poimirlem17  34440  poimirlem18  34441  poimirlem21  34444  poimirlem23  34446  poimirlem26  34449  poimirlem29  34452  poimirlem30  34453  poimirlem31  34454  poimir  34456  heicant  34458  mblfinlem2  34461  mblfinlem3  34462  itg2addnclem  34474  itg2addnclem2  34475  itg2gt0cn  34478  ftc1anclem5  34502  ftc1anclem6  34503  filbcmb  34547  nninfnub  34558  mettrifi  34564  geomcau  34566  istotbnd3  34581  sstotbnd2  34584  ismtybndlem  34616  heibor1lem  34619  heiborlem1  34621  heiborlem8  34628  heiborlem10  34630  heibor  34631  opidonOLD  34662  riscer  34798  crngohomfo  34816  keridl  34842  ispridl2  34848  ispridlc  34880  ac6s6  34982  eqvreltr  35373  dral1-o  35571  ax12indalem  35612  ax12inda2ALT  35613  lsatcveq0  35699  eqlkr3  35768  atlatmstc  35986  atlrelat1  35988  hlrelat2  36070  intnatN  36074  cvrexchlem  36086  cvratlem  36088  cvrat2  36096  atltcvr  36102  cvrat3  36109  cvrat4  36110  ps-1  36144  ps-2  36145  lplnnle2at  36208  lvolnle3at  36249  2llnma3r  36455  cdlemblem  36460  pmapjoin  36519  elpcliN  36560  lhpmcvr4N  36693  4atexlemnclw  36737  trlnidatb  36844  cdlemc4  36861  cdlemd3  36867  cdleme3g  36901  cdleme7d  36913  cdleme11c  36928  cdleme11dN  36929  cdleme21b  36993  cdleme21c  36994  cdleme21i  37002  cdleme22b  37008  cdleme35fnpq  37116  cdlemf1  37228  trlord  37236  cdlemg6c  37287  dihglblem6  38007  dochlkr  38052  dochkrshp  38053  dihjat1lem  38095  dochexmidlem5  38131  dochexmidlem8  38134  qsalrel  38655  fphpdo  38899  pellexlem5  38915  pellexlem6  38916  jm2.26lem3  39083  unxpwdom3  39180  iscard5  39386  ov2ssiunov2  39530  frege124d  39591  ordpss  40322  19.41rg  40423  stoweidlem34  41861  euoreqb  42824  2reu8i  42828  ralralimp  42993  f1oresf1o2  43006  zm1nn  43018  elfz2z  43031  iccpartlt  43066  iccelpart  43075  icceuelpartlem  43077  fargshiftf1  43083  sprsymrelf1lem  43135  paireqne  43155  reuopreuprim  43170  goldbachthlem2  43190  odz2prm2pw  43207  fmtnoprmfac1lem  43208  fmtnofac2lem  43212  prmdvdsfmtnof1  43231  sfprmdvdsmersenne  43250  lighneallem2  43253  lighneallem4  43257  fppr2odd  43378  gbegt5  43408  gbowge7  43410  bgoldbtbndlem4  43455  bgoldbtbnd  43456  tgoldbach  43464  isomuspgrlem2b  43476  isomgrsym  43483  zrtermorngc  43750  zrtermoringc  43819  lcosslsp  43973  lindslinindsimp1  43992  snlindsntor  44006  m1modmmod  44062  eenglngeehlnmlem2  44206  itsclc0yqsol  44232  itschlc0xyqsol1  44234  itschlc0xyqsol  44235  setrec1lem4  44273  aacllem  44382