Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30401 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  2184  alrimdd  2219  axc16g  2265  axc16nf  2268  axc11r  2370  sb4a  2482  2eu1  2648  2eu1v  2649  ss2ralv  4001  ss2rexv  4002  trel3  5211  poss  5531  sess2  5587  wefrc  5615  wereu2  5618  predtrss  6277  frpomin  6295  funun  6535  ssimaex  6916  f1cofveqaeq  7200  f1imass  7207  soisoi  7271  isores3  7278  isofrlem  7283  isoselem  7284  weniso  7297  abnexg  7698  oninton  7737  orduniorsuc  7769  limuni3  7791  tfindsg  7800  limom  7821  resf1extb  7873  f1o2ndf1  8061  soxp  8068  xpord3inddlem  8093  soseq  8098  extmptsuppeq  8127  smoel  8289  tfrlem9  8313  tz7.49  8373  seqomlem1  8378  odi  8503  omass  8504  omeulem2  8507  oeordsuc  8518  oeeulem  8525  naddsuc2  8625  ertr  8646  swoord2  8664  ecopovtrn  8753  domtriord  9047  pssnn  9089  unxpdomlem2  9152  isinf  9160  f1finf1o  9168  findcard3  9178  frfi  9180  unblem3  9189  supssd  9358  infssd  9389  en3lplem1  9513  inf3lem5  9533  cantnfle  9572  cantnfp1lem3  9581  ttrcltr  9617  frmin  9653  rankxpsuc  9786  tcrank  9788  ficardom  9865  carduni  9885  infxpenlem  9915  dfac8alem  9931  ac10ct  9936  ween  9937  alephdom  9983  alephle  9990  iscard3  9995  alephfp  10010  pwsdompw  10105  infdif  10110  cfslbn  10169  cofsmo  10171  cfcof  10176  fin1a2s  10316  domtriomlem  10344  ac6num  10381  zorn2lem3  10400  axdclem2  10422  imadomg  10436  iundom2g  10442  ficard  10467  fpwwe2lem7  10539  fpwwe2  10545  gchpwdom  10572  gchaclem  10580  tskr1om2  10670  inar1  10677  tskord  10682  tskuni  10685  grudomon  10719  grur1a  10721  grur1  10722  addnidpi  10803  ltexnq  10877  genpnnp  10907  addclprlem2  10919  mulclprlem  10921  psslinpr  10933  ltexprlem6  10943  ltexprlem7  10944  addcanpr  10948  mulgt0sr  11007  map2psrpr  11012  supsrlem  11013  axrrecex  11065  letr  11218  dedekind  11287  recex  11760  lemul12b  11989  mulgt1OLD  11991  fimaxre2  12078  lbreu  12083  nnrecgt0  12179  nnunb  12388  bndndx  12391  zeo  12569  uzind  12575  fzind  12581  fnn0ind  12582  suprfinzcl  12597  suprzcl2  12842  zmax  12849  rpnnen1lem5  12885  xrletr  13063  qbtwnre  13105  qsqueeze  13107  qextltlem  13108  xralrple  13111  xlesubadd  13169  supxrunb1  13225  icoshft  13380  zltaddlt1le  13412  fzen  13448  elfz0fzfz0  13540  elfzmlbp  13546  elfzo0z  13608  fzofzim  13616  fzo1fzo0n0  13622  elfzodifsumelfzo  13638  ssfzoulel  13667  modadd1  13819  modmul1  13838  uzrdgfni  13872  fsuppmapnn0fiub0  13907  fsuppmapnn0ub  13909  fsuppmapnn0fz  13910  seqf1olem1  13955  seqf1olem2  13956  expnbnd  14146  faclbnd4lem4  14210  hashgt23el  14338  seqcoll  14378  hashle2pr  14391  elss2prb  14402  ccatalpha  14508  swrdsbslen  14579  swrdspsleq  14580  swrdswrdlem  14618  swrdswrd  14619  pfxccatin12lem2a  14641  pfxccatin12lem1  14642  pfxccatin12lem3  14646  swrdccat3blem  14653  reuccatpfxs1lem  14660  repswswrd  14698  cshf1  14724  swrd2lsw  14866  sqeqd  15080  sqrmo  15165  cau3lem  15269  icodiamlt  15352  limsupbnd2  15397  lo1bdd2  15438  climuni  15466  rlimcn3  15504  mulcn2  15510  o1of2  15527  rlimo1  15531  lo1le  15566  iseralt  15599  cvgrat  15797  fprodss  15862  rpnnen2lem12  16141  ruclem3  16149  sqrt2irr  16165  p1modz1  16177  dvdsmodexp  16178  dvds2lem  16186  dvdslelem  16227  dvdsabseq  16231  divalglem8  16318  bitsinv1lem  16359  sadcaddlem  16375  smu01lem  16403  smueqlem  16408  bezoutlem4  16460  dfgcd2  16464  algcvga  16497  lcmfunsnlem1  16555  lcmfunsnlem2lem1  16556  lcmfunsnlem2lem2  16557  lcmfdvdsb  16561  coprmgcdb  16567  coprmdvds2  16572  coprmprod  16579  isprm3  16601  prmdvdsfz  16623  isprm5  16625  coprm  16629  rpexp12i  16642  phibndlem  16688  dfphi2  16692  eulerthlem2  16700  odzdvds  16714  iserodd  16754  pclem  16757  pcpremul  16762  pcqcl  16775  pcdvdsb  16788  pcprmpw2  16801  difsqpwdvds  16806  pcaddlem  16807  pcmptcl  16810  pcfac  16818  prmpwdvds  16823  unbenlem  16827  prmreclem1  16835  4sqlem17  16880  vdwmc2  16898  vdwlem9  16908  vdwlem10  16909  vdwlem13  16912  vdwnnlem3  16916  ramcl  16948  prmgaplem7  16976  mreiincl  17506  initoid  17916  termoid  17917  initoeu2lem1  17929  pospo  18257  resspos  18343  resstos  18344  dirge  18517  cyccom  19123  gsmsymgrfixlem1  19347  oddvdsnn0  19464  oddvds  19467  odcl2  19485  gexdvds  19504  sylow2alem2  19538  sylow2a  19539  efgi2  19645  efgsrel  19654  efgs1b  19656  imasabl  19796  cyggex2  19817  telgsums  19913  pgpfac1lem2  19997  pgpfac1lem3a  19998  pgpfac1lem3  19999  pgpfac1lem5  20001  zrtermorngc  20567  zrtermoringc  20599  lmodfopnelem2  20841  lssssr  20896  rnglidlmcl  21162  gzrngunitlem  21378  znunit  21509  frgpcyg  21519  lsmcss  21638  obselocv  21674  obslbs  21676  mhpvarcl  22082  cply1mul  22231  gsummoncoe1  22243  cpmatacl  22651  cpmatinvcl  22652  cpmatmcllem  22653  m2cpminvid2lem  22689  mp2pm2mplem4  22744  pm2mp  22760  chfacfisf  22789  chfacfisfcpmat  22790  chfacfscmul0  22793  chfacfpmmul0  22797  cayhamlem4  22823  ordtrest2lem  23138  leordtval2  23147  lecldbas  23154  cncls  23209  cncnp  23215  cnpresti  23223  lmcnp  23239  cnt0  23281  isreg2  23312  cmpsublem  23334  cmpsub  23335  tgcmp  23336  bwth  23345  dfconn2  23354  1stcfb  23380  1stcelcls  23396  islly2  23419  dislly  23432  reftr  23449  comppfsc  23467  kgencn2  23492  txcnp  23555  txindis  23569  txcmplem1  23576  txlm  23583  xkohaus  23588  cnmptcom  23613  kqfvima  23665  isr0  23672  fgss2  23809  fbasrn  23819  filuni  23820  ufilmax  23842  isufil2  23843  cfinufil  23863  fmfnfmlem1  23889  fmfnfmlem2  23890  fmfnfmlem4  23892  fmfnfm  23893  fmco  23896  flimopn  23910  hausflim  23916  flimrest  23918  fclsopn  23949  flimfnfcls  23963  alexsubALTlem2  23983  alexsubALTlem3  23984  alexsubALT  23986  ptcmplem2  23988  cnextcn  24002  symgtgp  24041  qustgplem  24056  tsmsres  24079  tsmsxplem1  24088  isucn2  24213  imasdsf1olem  24308  bldisj  24333  blssps  24359  blss  24360  metcnp3  24475  ngptgp  24571  nrginvrcn  24627  nmoleub  24666  xrsmopn  24748  icccmplem3  24760  reconnlem2  24763  rectbntr0  24768  rescncf  24837  iocopnst  24884  iccpnfcnv  24889  lebnumii  24912  nmoleub2lem  25061  nmhmcn  25067  iscfil3  25220  iscau2  25224  iscau3  25225  iscau4  25226  iscmet3lem2  25239  caussi  25244  equivcfil  25246  equivcau  25247  ivthlem2  25400  ivthlem3  25401  ovoliunlem2  25451  ovoliunnul  25455  ioombl1lem4  25509  dyadmax  25546  dyadmbl  25548  volsup2  25553  itg2le  25687  itg2const2  25689  itg2seq  25690  itgsplitioo  25786  rolle  25941  c1lip1  25949  dvivthlem1  25960  lhop1  25966  dvcnvrelem1  25969  dvfsumrlim  25985  ply1divmo  26088  ig1peu  26127  plypf1  26164  coeaddlem  26201  dvply2g  26239  fta1  26263  quotcan  26264  aalioulem4  26290  ulmcaulem  26350  ulmcn  26355  pilem2  26409  sincosq1lem  26453  sinq12gt0  26463  sinq12ge0  26464  tanord1  26493  lognegb  26546  logrec  26720  logbgcd1irr  26751  dcubic  26803  xrlimcnp  26925  o1cxp  26932  ftalem2  27031  ftalem3  27032  fsumdvdscom  27142  chtub  27170  vmasum  27174  bcmono  27235  bposlem3  27244  bposlem7  27248  lgsdir  27290  lgsqrlem2  27305  lgsqrmodndvds  27311  gausslemma2dlem6  27330  gausslemma2d  27332  lgsquadlem2  27339  2lgslem3a1  27358  2lgslem3b1  27359  2lgslem3c1  27360  2lgslem3d1  27361  2sqlem6  27381  2sq2  27391  2sqmod  27394  dchrisumlem3  27449  pntrsumbnd2  27525  pntpbnd1  27544  pntibnd  27551  pntlem3  27567  pntleml  27569  sltres  27621  nosepon  27624  nolesgn2o  27630  nogesgn1o  27632  nodenselem8  27650  nosupbnd1lem1  27667  madess  27841  madebdaylemlrcut  27864  peano5uzs  28348  brbtwn2  28904  colinearalg  28909  axcontlem10  28972  edgupgr  29133  edglnl  29142  usgruspgrb  29182  subupgr  29286  uhgrspan1  29302  usgredgsscusgredg  29459  fusgrn0degnn0  29499  upgrewlkle2  29606  uspgr2wlkeq  29645  redwlk  29670  wlkdlem2  29681  upgrwlkdvdelem  29735  pthdlem1  29765  pthdlem2  29767  crctcshwlkn0lem3  29811  wlkiswwlks1  29866  wwlksm1edg  29880  wwlksnred  29891  wwlksnextbi  29893  umgr2adedgspth  29947  clwlkclwwlklem2fv2  29997  clwlkclwwlklem2a  29999  clwlkclwwlkf1lem3  30007  clwwisshclwwslemlem  30014  clwwlkf  30048  clwwlkext2edg  30057  wwlksubclwwlk  30059  clwwlknonex2lem2  30109  eupth2lems  30239  frgrwopreglem4a  30311  frgrregorufrg  30327  ex-natded5.3-2  30409  isgrpo  30498  vacn  30695  ubthlem2  30872  htthlem  30918  normgt0  31128  shmodsi  31390  spansneleq  31571  h1datomi  31582  nmcexi  32027  pjnormssi  32169  stm1add3i  32248  golem2  32273  cvnsym  32291  dmdmd  32301  mdslmd1lem1  32326  mdslmd1i  32330  mdexchi  32336  atcveq0  32349  superpos  32355  hatomistici  32363  atoml2i  32384  atcvat2i  32388  chirredlem1  32391  atcvat3i  32397  mdsymlem3  32406  mdsymlem5  32408  cdj3lem2b  32438  cdj3i  32442  submarchi  33196  dfufd2  33559  tpr2rico  33997  ordtrest2NEWlem  34007  xrge0iifcnv  34018  omssubadd  34385  eulerpartlemb  34453  ballotlemfc0  34578  ballotlemfcc  34579  ftc2re  34683  fissorduni  35173  loop1cycl  35253  subfacp1lem6  35301  iccllysconn  35366  cvmfolem  35395  satfsschain  35480  satfrel  35483  satfdm  35485  sat1el2xp  35495  satffunlem1lem1  35518  dmopab3rexdif  35521  satffunlem2lem2  35522  satffun  35525  fundmpss  35883  dfon2lem3  35899  dfon2lem6  35902  axextbdist  35914  dfrdg4  36067  5segofs  36122  cgrextend  36124  segconeu  36127  btwncomim  36129  btwnswapid  36133  btwnintr  36135  btwnexch3  36136  btwndiff  36143  ifscgr  36160  cgrxfr  36171  btwnxfr  36172  lineext  36192  brofs2  36193  linecgr  36197  lineid  36199  idinside  36200  endofsegid  36201  btwnconn1lem13  36215  btwnconn3  36219  finminlem  36434  nn0prpwlem  36438  cldbnd  36442  clsint2  36445  fnessref  36473  neibastop3  36478  fgmin  36486  onsuct0  36557  limsucncmpi  36561  bj-nnfea  36851  bj-axc14  36973  bj-restn0  37207  bj-0int  37218  wl-19.2reqv  37641  wl-aetr  37646  wl-axc11r  37647  fin2so  37720  tan2h  37725  lindsenlbs  37728  poimirlem2  37735  poimirlem9  37742  poimirlem17  37750  poimirlem18  37751  poimirlem21  37754  poimirlem23  37756  poimirlem26  37759  poimirlem29  37762  poimirlem30  37763  poimirlem31  37764  poimir  37766  heicant  37768  mblfinlem2  37771  mblfinlem3  37772  itg2addnclem  37784  itg2addnclem2  37785  itg2gt0cn  37788  ftc1anclem5  37810  ftc1anclem6  37811  filbcmb  37853  nninfnub  37864  mettrifi  37870  geomcau  37872  istotbnd3  37884  sstotbnd2  37887  ismtybndlem  37919  heibor1lem  37922  heiborlem1  37924  heiborlem8  37931  heiborlem10  37933  heibor  37934  opidonOLD  37965  riscer  38101  crngohomfo  38119  keridl  38145  ispridl2  38151  ispridlc  38183  ac6s6  38285  eqvreltr  38776  dral1-o  39076  ax12indalem  39117  ax12inda2ALT  39118  lsatcveq0  39204  eqlkr3  39273  atlatmstc  39491  atlrelat1  39493  hlrelat2  39575  intnatN  39579  cvrexchlem  39591  cvratlem  39593  cvrat2  39601  atltcvr  39607  cvrat3  39614  cvrat4  39615  ps-1  39649  ps-2  39650  lplnnle2at  39713  lvolnle3at  39754  2llnma3r  39960  cdlemblem  39965  pmapjoin  40024  elpcliN  40065  lhpmcvr4N  40198  4atexlemnclw  40242  trlnidatb  40349  cdlemc4  40366  cdlemd3  40372  cdleme3g  40406  cdleme7d  40418  cdleme11c  40433  cdleme11dN  40434  cdleme21b  40498  cdleme21c  40499  cdleme21i  40507  cdleme22b  40513  cdleme35fnpq  40621  cdlemf1  40733  trlord  40741  cdlemg6c  40792  dihglblem6  41512  dochlkr  41557  dochkrshp  41558  dihjat1lem  41600  dochexmidlem5  41636  dochexmidlem8  41639  qsalrel  42411  remulcand  42609  prjspner1  42784  fphpdo  42974  pellexlem5  42990  pellexlem6  42991  jm2.26lem3  43158  unxpwdom3  43252  omlimcl2  43399  oe0suclim  43434  cantnfresb  43481  tfsconcatb0  43501  naddgeoa  43551  iscard5  43693  sqrtcval  43798  ov2ssiunov2  43857  frege124d  43918  ordpss  44607  19.41rg  44707  relpfrlem  45110  modelaxreplem2  45136  stoweidlem34  46194  ormklocald  47034  evenwodadd  47047  cfsetsnfsetf1  47221  fcoresf1  47231  euoreqb  47271  2reu8i  47275  ralralimp  47440  f1oresf1o2  47453  zm1nn  47464  elfz2z  47477  2tceilhalfelfzo1  47494  m1modmmod  47520  modlt0b  47525  iccpartlt  47586  iccelpart  47595  icceuelpartlem  47597  fargshiftf1  47603  sprsymrelf1lem  47653  paireqne  47673  reuopreuprim  47688  goldbachthlem2  47708  odz2prm2pw  47725  fmtnoprmfac1lem  47726  fmtnofac2lem  47730  prmdvdsfmtnof1  47749  sfprmdvdsmersenne  47765  lighneallem2  47768  lighneallem4  47772  fppr2odd  47893  gbegt5  47923  gbowge7  47925  bgoldbtbndlem4  47970  bgoldbtbnd  47971  tgoldbach  47979  grimuhgr  48049  grimcnv  48050  grimco  48051  isuspgrim0  48056  isuspgrimlem  48057  upgrimwlklem5  48063  upgrimtrlslem2  48067  uhgrimisgrgriclem  48092  clnbgrgrimlem  48095  clnbgrgrim  48096  grimedg  48097  grtriprop  48103  isubgr3stgrlem3  48130  isubgr3stgrlem4  48131  isubgr3stgrlem6  48133  isubgr3stgrlem7  48134  uspgrlimlem3  48152  grlimedgclnbgr  48157  grlimgrtrilem2  48164  grlimgrtri  48165  grlicsym  48175  gpgedgvtx1  48224  gpgedgiov  48227  gpgedg2ov  48228  gpgedg2iv  48229  pgnioedg1  48270  pgnioedg2  48271  pgnioedg3  48272  pgnioedg4  48273  pgnioedg5  48274  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  pgnbgreunbgrlem5lem1  48282  pgnbgreunbgrlem5lem2  48283  pgnbgreunbgrlem5lem3  48284  lcosslsp  48600  lindslinindsimp1  48619  snlindsntor  48633  itcovalt2  48839  eenglngeehlnmlem2  48900  itsclc0yqsol  48926  itschlc0xyqsol1  48928  itschlc0xyqsol  48929  opnneilv  49070  i0oii  49081  io1ii  49082  iscnrm3lem4  49097  iscnrm3r  49109  setrec1lem4  49851  aacllem  49962