Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30347 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  156  pm2.61d  179  sylibd  239  sylbid  240  sylibrd  259  sylbird  260  syland  603  animpimp2impd  846  ax12v2  2178  alrimdd  2213  axc16g  2259  axc16nf  2262  axc11r  2369  sb4a  2483  2eu1  2649  2eu1v  2650  ss2ralv  4034  ss2rexv  4035  trel3  5249  poss  5574  sess2  5631  wefrc  5659  wereu2  5662  predtrss  6322  frpomin  6340  funun  6592  ssimaex  6974  f1cofveqaeq  7260  f1imass  7266  soisoi  7330  isores3  7337  isofrlem  7342  isoselem  7343  weniso  7356  abnexg  7758  oninton  7797  orduniorsuc  7832  limuni3  7855  tfindsg  7864  limom  7885  resf1extb  7938  f1o2ndf1  8129  soxp  8136  xpord3inddlem  8161  soseq  8166  extmptsuppeq  8195  smoel  8382  tfrlem9  8407  tz7.49  8467  seqomlem1  8472  odi  8599  omass  8600  omeulem2  8603  oeordsuc  8614  oeeulem  8621  naddsuc2  8721  ertr  8742  swoord2  8760  ecopovtrn  8842  domtriord  9145  pssnn  9190  onomeneqOLD  9248  unxpdomlem2  9269  isinf  9278  isinfOLD  9279  f1finf1o  9287  findcard3  9300  findcard3OLD  9301  frfi  9303  unblem3  9312  en3lplem1  9634  inf3lem5  9654  cantnfle  9693  cantnfp1lem3  9702  ttrcltr  9738  frmin  9771  rankxpsuc  9904  tcrank  9906  ficardom  9983  carduni  10003  infxpenlem  10035  dfac8alem  10051  ac10ct  10056  ween  10057  alephdom  10103  alephle  10110  iscard3  10115  alephfp  10130  pwsdompw  10225  infdif  10230  cfslbn  10289  cofsmo  10291  cfcof  10296  fin1a2s  10436  domtriomlem  10464  ac6num  10501  zorn2lem3  10520  axdclem2  10542  imadomg  10556  iundom2g  10562  ficard  10587  fpwwe2lem7  10659  fpwwe2  10665  gchpwdom  10692  gchaclem  10700  tskr1om2  10790  inar1  10797  tskord  10802  tskuni  10805  grudomon  10839  grur1a  10841  grur1  10842  addnidpi  10923  ltexnq  10997  genpnnp  11027  addclprlem2  11039  mulclprlem  11041  psslinpr  11053  ltexprlem6  11063  ltexprlem7  11064  addcanpr  11068  mulgt0sr  11127  map2psrpr  11132  supsrlem  11133  axrrecex  11185  letr  11337  dedekind  11406  recex  11877  lemul12b  12106  mulgt1OLD  12108  fimaxre2  12195  lbreu  12200  nnrecgt0  12291  nnunb  12505  bndndx  12508  zeo  12687  uzind  12693  fzind  12699  fnn0ind  12700  suprfinzcl  12715  suprzcl2  12962  zmax  12969  rpnnen1lem5  13005  xrletr  13182  qbtwnre  13223  qsqueeze  13225  qextltlem  13226  xralrple  13229  xlesubadd  13287  supxrunb1  13343  icoshft  13495  zltaddlt1le  13527  fzen  13563  elfz0fzfz0  13655  elfzmlbp  13661  elfzo0z  13723  fzofzim  13731  fzo1fzo0n0  13736  elfzodifsumelfzo  13752  ssfzoulel  13781  modadd1  13930  modmul1  13947  uzrdgfni  13981  fsuppmapnn0fiub0  14016  fsuppmapnn0ub  14018  fsuppmapnn0fz  14019  seqf1olem1  14064  seqf1olem2  14065  expnbnd  14253  faclbnd4lem4  14317  hashgt23el  14445  seqcoll  14485  hashle2pr  14498  elss2prb  14509  ccatalpha  14613  swrdsbslen  14684  swrdspsleq  14685  swrdswrdlem  14724  swrdswrd  14725  pfxccatin12lem2a  14747  pfxccatin12lem1  14748  pfxccatin12lem3  14752  swrdccat3blem  14759  reuccatpfxs1lem  14766  repswswrd  14804  cshf1  14830  swrd2lsw  14973  sqeqd  15187  sqrmo  15272  cau3lem  15375  icodiamlt  15456  limsupbnd2  15501  lo1bdd2  15542  climuni  15570  rlimcn3  15608  mulcn2  15614  o1of2  15631  rlimo1  15635  lo1le  15670  iseralt  15703  cvgrat  15901  fprodss  15966  rpnnen2lem12  16243  ruclem3  16251  sqrt2irr  16267  p1modz1  16279  dvdsmodexp  16280  dvds2lem  16288  dvdslelem  16328  dvdsabseq  16332  divalglem8  16419  bitsinv1lem  16460  sadcaddlem  16476  smu01lem  16504  smueqlem  16509  bezoutlem4  16561  dfgcd2  16565  algcvga  16598  lcmfunsnlem1  16656  lcmfunsnlem2lem1  16657  lcmfunsnlem2lem2  16658  lcmfdvdsb  16662  coprmgcdb  16668  coprmdvds2  16673  coprmprod  16680  isprm3  16702  prmdvdsfz  16724  isprm5  16726  coprm  16730  rpexp12i  16743  phibndlem  16789  dfphi2  16793  eulerthlem2  16801  odzdvds  16815  iserodd  16855  pclem  16858  pcpremul  16863  pcqcl  16876  pcdvdsb  16889  pcprmpw2  16902  difsqpwdvds  16907  pcaddlem  16908  pcmptcl  16911  pcfac  16919  prmpwdvds  16924  unbenlem  16928  prmreclem1  16936  4sqlem17  16981  vdwmc2  16999  vdwlem9  17009  vdwlem10  17010  vdwlem13  17013  vdwnnlem3  17017  ramcl  17049  prmgaplem7  17077  mreiincl  17610  initoid  18017  termoid  18018  initoeu2lem1  18030  pospo  18359  dirge  18617  cyccom  19190  gsmsymgrfixlem1  19413  oddvdsnn0  19530  oddvds  19533  odcl2  19551  gexdvds  19570  sylow2alem2  19604  sylow2a  19605  efgi2  19711  efgsrel  19720  efgs1b  19722  imasabl  19862  cyggex2  19883  telgsums  19979  pgpfac1lem2  20063  pgpfac1lem3a  20064  pgpfac1lem3  20065  pgpfac1lem5  20067  zrtermorngc  20611  zrtermoringc  20643  lmodfopnelem2  20865  lssssr  20920  rnglidlmcl  21188  gzrngunitlem  21412  znunit  21536  frgpcyg  21546  lsmcss  21664  obselocv  21702  obslbs  21704  mhpvarcl  22100  cply1mul  22248  gsummoncoe1  22260  cpmatacl  22670  cpmatinvcl  22671  cpmatmcllem  22672  m2cpminvid2lem  22708  mp2pm2mplem4  22763  pm2mp  22779  chfacfisf  22808  chfacfisfcpmat  22809  chfacfscmul0  22812  chfacfpmmul0  22816  cayhamlem4  22842  ordtrest2lem  23157  leordtval2  23166  lecldbas  23173  cncls  23228  cncnp  23234  cnpresti  23242  lmcnp  23258  cnt0  23300  isreg2  23331  cmpsublem  23353  cmpsub  23354  tgcmp  23355  bwth  23364  dfconn2  23373  1stcfb  23399  1stcelcls  23415  islly2  23438  dislly  23451  reftr  23468  comppfsc  23486  kgencn2  23511  txcnp  23574  txindis  23588  txcmplem1  23595  txlm  23602  xkohaus  23607  cnmptcom  23632  kqfvima  23684  isr0  23691  fgss2  23828  fbasrn  23838  filuni  23839  ufilmax  23861  isufil2  23862  cfinufil  23882  fmfnfmlem1  23908  fmfnfmlem2  23909  fmfnfmlem4  23911  fmfnfm  23912  fmco  23915  flimopn  23929  hausflim  23935  flimrest  23937  fclsopn  23968  flimfnfcls  23982  alexsubALTlem2  24002  alexsubALTlem3  24003  alexsubALT  24005  ptcmplem2  24007  cnextcn  24021  symgtgp  24060  qustgplem  24075  tsmsres  24098  tsmsxplem1  24107  isucn2  24233  imasdsf1olem  24328  bldisj  24353  blssps  24379  blss  24380  metcnp3  24497  ngptgp  24593  nrginvrcn  24649  nmoleub  24688  xrsmopn  24770  icccmplem3  24782  reconnlem2  24785  rectbntr0  24790  rescncf  24859  iocopnst  24906  iccpnfcnv  24911  lebnumii  24934  nmoleub2lem  25083  nmhmcn  25089  iscfil3  25243  iscau2  25247  iscau3  25248  iscau4  25249  iscmet3lem2  25262  caussi  25267  equivcfil  25269  equivcau  25270  ivthlem2  25423  ivthlem3  25424  ovoliunlem2  25474  ovoliunnul  25478  ioombl1lem4  25532  dyadmax  25569  dyadmbl  25571  volsup2  25576  itg2le  25710  itg2const2  25712  itg2seq  25713  itgsplitioo  25809  rolle  25964  c1lip1  25972  dvivthlem1  25983  lhop1  25989  dvcnvrelem1  25992  dvfsumrlim  26008  ply1divmo  26111  ig1peu  26150  plypf1  26187  coeaddlem  26224  dvply2g  26262  fta1  26286  quotcan  26287  aalioulem4  26313  ulmcaulem  26373  ulmcn  26378  pilem2  26432  sincosq1lem  26475  sinq12gt0  26485  sinq12ge0  26486  tanord1  26515  lognegb  26568  logrec  26742  logbgcd1irr  26773  dcubic  26825  xrlimcnp  26947  o1cxp  26954  ftalem2  27053  ftalem3  27054  fsumdvdscom  27164  chtub  27192  vmasum  27196  bcmono  27257  bposlem3  27266  bposlem7  27270  lgsdir  27312  lgsqrlem2  27327  lgsqrmodndvds  27333  gausslemma2dlem6  27352  gausslemma2d  27354  lgsquadlem2  27361  2lgslem3a1  27380  2lgslem3b1  27381  2lgslem3c1  27382  2lgslem3d1  27383  2sqlem6  27403  2sq2  27413  2sqmod  27416  dchrisumlem3  27471  pntrsumbnd2  27547  pntpbnd1  27566  pntibnd  27573  pntlem3  27589  pntleml  27591  sltres  27643  nosepon  27646  nolesgn2o  27652  nogesgn1o  27654  nodenselem8  27672  nosupbnd1lem1  27689  madess  27851  madebdaylemlrcut  27873  peano5uzs  28326  brbtwn2  28850  colinearalg  28855  axcontlem10  28918  edgupgr  29079  edglnl  29088  usgruspgrb  29128  subupgr  29232  uhgrspan1  29248  usgredgsscusgredg  29405  fusgrn0degnn0  29445  upgrewlkle2  29552  uspgr2wlkeq  29592  redwlk  29618  wlkdlem2  29629  upgrwlkdvdelem  29684  pthdlem1  29714  pthdlem2  29716  crctcshwlkn0lem3  29760  wlkiswwlks1  29815  wwlksm1edg  29829  wwlksnred  29840  wwlksnextbi  29842  umgr2adedgspth  29896  clwlkclwwlklem2fv2  29943  clwlkclwwlklem2a  29945  clwlkclwwlkf1lem3  29953  clwwisshclwwslemlem  29960  clwwlkf  29994  clwwlkext2edg  30003  wwlksubclwwlk  30005  clwwlknonex2lem2  30055  eupth2lems  30185  frgrwopreglem4a  30257  frgrregorufrg  30273  ex-natded5.3-2  30355  isgrpo  30444  vacn  30641  ubthlem2  30818  htthlem  30864  normgt0  31074  shmodsi  31336  spansneleq  31517  h1datomi  31528  nmcexi  31973  pjnormssi  32115  stm1add3i  32194  golem2  32219  cvnsym  32237  dmdmd  32247  mdslmd1lem1  32272  mdslmd1i  32276  mdexchi  32282  atcveq0  32295  superpos  32301  hatomistici  32309  atoml2i  32330  atcvat2i  32334  chirredlem1  32337  atcvat3i  32343  mdsymlem3  32352  mdsymlem5  32354  cdj3lem2b  32384  cdj3i  32388  supssd  32656  infssd  32657  resspos  32895  resstos  32896  submarchi  33132  dfufd2  33513  tpr2rico  33870  ordtrest2NEWlem  33880  xrge0iifcnv  33891  omssubadd  34261  eulerpartlemb  34329  ballotlemfc0  34454  ballotlemfcc  34455  ftc2re  34572  loop1cycl  35101  subfacp1lem6  35149  iccllysconn  35214  cvmfolem  35243  satfsschain  35328  satfrel  35331  satfdm  35333  sat1el2xp  35343  satffunlem1lem1  35366  dmopab3rexdif  35369  satffunlem2lem2  35370  satffun  35373  fundmpss  35726  dfon2lem3  35745  dfon2lem6  35748  axextbdist  35760  dfrdg4  35911  5segofs  35966  cgrextend  35968  segconeu  35971  btwncomim  35973  btwnswapid  35977  btwnintr  35979  btwnexch3  35980  btwndiff  35987  ifscgr  36004  cgrxfr  36015  btwnxfr  36016  lineext  36036  brofs2  36037  linecgr  36041  lineid  36043  idinside  36044  endofsegid  36045  btwnconn1lem13  36059  btwnconn3  36063  finminlem  36278  nn0prpwlem  36282  cldbnd  36286  clsint2  36289  fnessref  36317  neibastop3  36322  fgmin  36330  onsuct0  36401  limsucncmpi  36405  bj-nnfea  36694  bj-axc14  36816  bj-restn0  37050  bj-0int  37061  wl-19.2reqv  37484  wl-aetr  37489  wl-axc11r  37490  fin2so  37573  tan2h  37578  lindsenlbs  37581  poimirlem2  37588  poimirlem9  37595  poimirlem17  37603  poimirlem18  37604  poimirlem21  37607  poimirlem23  37609  poimirlem26  37612  poimirlem29  37615  poimirlem30  37616  poimirlem31  37617  poimir  37619  heicant  37621  mblfinlem2  37624  mblfinlem3  37625  itg2addnclem  37637  itg2addnclem2  37638  itg2gt0cn  37641  ftc1anclem5  37663  ftc1anclem6  37664  filbcmb  37706  nninfnub  37717  mettrifi  37723  geomcau  37725  istotbnd3  37737  sstotbnd2  37740  ismtybndlem  37772  heibor1lem  37775  heiborlem1  37777  heiborlem8  37784  heiborlem10  37786  heibor  37787  opidonOLD  37818  riscer  37954  crngohomfo  37972  keridl  37998  ispridl2  38004  ispridlc  38036  ac6s6  38138  eqvreltr  38567  dral1-o  38864  ax12indalem  38905  ax12inda2ALT  38906  lsatcveq0  38992  eqlkr3  39061  atlatmstc  39279  atlrelat1  39281  hlrelat2  39364  intnatN  39368  cvrexchlem  39380  cvratlem  39382  cvrat2  39390  atltcvr  39396  cvrat3  39403  cvrat4  39404  ps-1  39438  ps-2  39439  lplnnle2at  39502  lvolnle3at  39543  2llnma3r  39749  cdlemblem  39754  pmapjoin  39813  elpcliN  39854  lhpmcvr4N  39987  4atexlemnclw  40031  trlnidatb  40138  cdlemc4  40155  cdlemd3  40161  cdleme3g  40195  cdleme7d  40207  cdleme11c  40222  cdleme11dN  40223  cdleme21b  40287  cdleme21c  40288  cdleme21i  40296  cdleme22b  40302  cdleme35fnpq  40410  cdlemf1  40522  trlord  40530  cdlemg6c  40581  dihglblem6  41301  dochlkr  41346  dochkrshp  41347  dihjat1lem  41389  dochexmidlem5  41425  dochexmidlem8  41428  metakunt29  42193  qsalrel  42239  remulcand  42431  prjspner1  42599  fphpdo  42791  pellexlem5  42807  pellexlem6  42808  jm2.26lem3  42976  unxpwdom3  43070  omlimcl2  43217  oe0suclim  43252  cantnfresb  43299  tfsconcatb0  43319  naddgeoa  43369  iscard5  43511  sqrtcval  43616  ov2ssiunov2  43675  frege124d  43736  ordpss  44427  19.41rg  44527  relpfrlem  44931  modelaxreplem2  44953  stoweidlem34  46006  ormklocald  46846  evenwodadd  46860  cfsetsnfsetf1  47029  fcoresf1  47039  euoreqb  47079  2reu8i  47083  ralralimp  47248  f1oresf1o2  47261  zm1nn  47272  elfz2z  47285  iccpartlt  47369  iccelpart  47378  icceuelpartlem  47380  fargshiftf1  47386  sprsymrelf1lem  47436  paireqne  47456  reuopreuprim  47471  goldbachthlem2  47491  odz2prm2pw  47508  fmtnoprmfac1lem  47509  fmtnofac2lem  47513  prmdvdsfmtnof1  47532  sfprmdvdsmersenne  47548  lighneallem2  47551  lighneallem4  47555  fppr2odd  47676  gbegt5  47706  gbowge7  47708  bgoldbtbndlem4  47753  bgoldbtbnd  47754  tgoldbach  47762  isuspgrim0  47830  isuspgrimlem  47832  grimuhgr  47836  grimcnv  47837  grimco  47838  uhgrimisgrgriclem  47856  clnbgrgrimlem  47859  clnbgrgrim  47860  grimedg  47861  grtriprop  47866  isubgr3stgrlem3  47893  isubgr3stgrlem4  47894  isubgr3stgrlem6  47896  isubgr3stgrlem7  47897  uspgrlimlem3  47915  grlimgrtrilem2  47920  grlimgrtri  47921  grlicsym  47931  2tceilhalfelfzo1  47976  gpgedgvtx1  47978  lcosslsp  48313  lindslinindsimp1  48332  snlindsntor  48346  m1modmmod  48400  itcovalt2  48556  eenglngeehlnmlem2  48617  itsclc0yqsol  48643  itschlc0xyqsol1  48645  itschlc0xyqsol  48646  opnneilv  48766  i0oii  48777  io1ii  48778  iscnrm3lem4  48793  iscnrm3r  48805  setrec1lem4  49217  aacllem  49328