Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30487 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  604  animpimp2impd  847  ax12v2  2187  alrimdd  2222  axc16g  2268  axc16nf  2271  axc11r  2373  sb4a  2485  2eu1  2652  2eu1v  2653  ss2ralv  4006  ss2rexv  4007  trel3  5216  poss  5542  sess2  5598  wefrc  5626  wereu2  5629  predtrss  6288  frpomin  6306  funun  6546  ssimaex  6927  f1cofveqaeq  7213  f1imass  7220  soisoi  7284  isores3  7291  isofrlem  7296  isoselem  7297  weniso  7310  abnexg  7711  oninton  7750  orduniorsuc  7782  limuni3  7804  tfindsg  7813  limom  7834  resf1extb  7886  f1o2ndf1  8074  soxp  8081  xpord3inddlem  8106  soseq  8111  extmptsuppeq  8140  smoel  8302  tfrlem9  8326  tz7.49  8386  seqomlem1  8391  odi  8516  omass  8517  omeulem2  8520  oeordsuc  8532  oeeulem  8539  naddsuc2  8639  ertr  8661  swoord2  8679  ecopovtrn  8769  domtriord  9063  pssnn  9105  unxpdomlem2  9169  isinf  9177  f1finf1o  9185  findcard3  9195  frfi  9197  unblem3  9206  supssd  9378  infssd  9409  en3lplem1  9533  inf3lem5  9553  cantnfle  9592  cantnfp1lem3  9601  ttrcltr  9637  frmin  9673  rankxpsuc  9806  tcrank  9808  ficardom  9885  carduni  9905  infxpenlem  9935  dfac8alem  9951  ac10ct  9956  ween  9957  alephdom  10003  alephle  10010  iscard3  10015  alephfp  10030  pwsdompw  10125  infdif  10130  cfslbn  10189  cofsmo  10191  cfcof  10196  fin1a2s  10336  domtriomlem  10364  ac6num  10401  zorn2lem3  10420  axdclem2  10442  imadomg  10456  iundom2g  10462  ficard  10487  fpwwe2lem7  10560  fpwwe2  10566  gchpwdom  10593  gchaclem  10601  tskr1om2  10691  inar1  10698  tskord  10703  tskuni  10706  grudomon  10740  grur1a  10742  grur1  10743  addnidpi  10824  ltexnq  10898  genpnnp  10928  addclprlem2  10940  mulclprlem  10942  psslinpr  10954  ltexprlem6  10964  ltexprlem7  10965  addcanpr  10969  mulgt0sr  11028  map2psrpr  11033  supsrlem  11034  axrrecex  11086  letr  11239  dedekind  11308  recex  11781  lemul12b  12010  mulgt1OLD  12012  fimaxre2  12099  lbreu  12104  nnrecgt0  12200  nnunb  12409  bndndx  12412  zeo  12590  uzind  12596  fzind  12602  fnn0ind  12603  suprfinzcl  12618  suprzcl2  12863  zmax  12870  rpnnen1lem5  12906  xrletr  13084  qbtwnre  13126  qsqueeze  13128  qextltlem  13129  xralrple  13132  xlesubadd  13190  supxrunb1  13246  icoshft  13401  zltaddlt1le  13433  fzen  13469  elfz0fzfz0  13561  elfzmlbp  13567  elfzo0z  13629  fzofzim  13637  fzo1fzo0n0  13643  elfzodifsumelfzo  13659  ssfzoulel  13688  modadd1  13840  modmul1  13859  uzrdgfni  13893  fsuppmapnn0fiub0  13928  fsuppmapnn0ub  13930  fsuppmapnn0fz  13931  seqf1olem1  13976  seqf1olem2  13977  expnbnd  14167  faclbnd4lem4  14231  hashgt23el  14359  seqcoll  14399  hashle2pr  14412  elss2prb  14423  ccatalpha  14529  swrdsbslen  14600  swrdspsleq  14601  swrdswrdlem  14639  swrdswrd  14640  pfxccatin12lem2a  14662  pfxccatin12lem1  14663  pfxccatin12lem3  14667  swrdccat3blem  14674  reuccatpfxs1lem  14681  repswswrd  14719  cshf1  14745  swrd2lsw  14887  sqeqd  15101  sqrmo  15186  cau3lem  15290  icodiamlt  15373  limsupbnd2  15418  lo1bdd2  15459  climuni  15487  rlimcn3  15525  mulcn2  15531  o1of2  15548  rlimo1  15552  lo1le  15587  iseralt  15620  cvgrat  15818  fprodss  15883  rpnnen2lem12  16162  ruclem3  16170  sqrt2irr  16186  p1modz1  16198  dvdsmodexp  16199  dvds2lem  16207  dvdslelem  16248  dvdsabseq  16252  divalglem8  16339  bitsinv1lem  16380  sadcaddlem  16396  smu01lem  16424  smueqlem  16429  bezoutlem4  16481  dfgcd2  16485  algcvga  16518  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfdvdsb  16582  coprmgcdb  16588  coprmdvds2  16593  coprmprod  16600  isprm3  16622  prmdvdsfz  16644  isprm5  16646  coprm  16650  rpexp12i  16663  phibndlem  16709  dfphi2  16713  eulerthlem2  16721  odzdvds  16735  iserodd  16775  pclem  16778  pcpremul  16783  pcqcl  16796  pcdvdsb  16809  pcprmpw2  16822  difsqpwdvds  16827  pcaddlem  16828  pcmptcl  16831  pcfac  16839  prmpwdvds  16844  unbenlem  16848  prmreclem1  16856  4sqlem17  16901  vdwmc2  16919  vdwlem9  16929  vdwlem10  16930  vdwlem13  16933  vdwnnlem3  16937  ramcl  16969  prmgaplem7  16997  mreiincl  17527  initoid  17937  termoid  17938  initoeu2lem1  17950  pospo  18278  resspos  18364  resstos  18365  dirge  18538  cyccom  19144  gsmsymgrfixlem1  19368  oddvdsnn0  19485  oddvds  19488  odcl2  19506  gexdvds  19525  sylow2alem2  19559  sylow2a  19560  efgi2  19666  efgsrel  19675  efgs1b  19677  imasabl  19817  cyggex2  19838  telgsums  19934  pgpfac1lem2  20018  pgpfac1lem3a  20019  pgpfac1lem3  20020  pgpfac1lem5  20022  zrtermorngc  20588  zrtermoringc  20620  lmodfopnelem2  20862  lssssr  20917  rnglidlmcl  21183  gzrngunitlem  21399  znunit  21530  frgpcyg  21540  lsmcss  21659  obselocv  21695  obslbs  21697  mhpvarcl  22103  cply1mul  22252  gsummoncoe1  22264  cpmatacl  22672  cpmatinvcl  22673  cpmatmcllem  22674  m2cpminvid2lem  22710  mp2pm2mplem4  22765  pm2mp  22781  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmul0  22814  chfacfpmmul0  22818  cayhamlem4  22844  ordtrest2lem  23159  leordtval2  23168  lecldbas  23175  cncls  23230  cncnp  23236  cnpresti  23244  lmcnp  23260  cnt0  23302  isreg2  23333  cmpsublem  23355  cmpsub  23356  tgcmp  23357  bwth  23366  dfconn2  23375  1stcfb  23401  1stcelcls  23417  islly2  23440  dislly  23453  reftr  23470  comppfsc  23488  kgencn2  23513  txcnp  23576  txindis  23590  txcmplem1  23597  txlm  23604  xkohaus  23609  cnmptcom  23634  kqfvima  23686  isr0  23693  fgss2  23830  fbasrn  23840  filuni  23841  ufilmax  23863  isufil2  23864  cfinufil  23884  fmfnfmlem1  23910  fmfnfmlem2  23911  fmfnfmlem4  23913  fmfnfm  23914  fmco  23917  flimopn  23931  hausflim  23937  flimrest  23939  fclsopn  23970  flimfnfcls  23984  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALT  24007  ptcmplem2  24009  cnextcn  24023  symgtgp  24062  qustgplem  24077  tsmsres  24100  tsmsxplem1  24109  isucn2  24234  imasdsf1olem  24329  bldisj  24354  blssps  24380  blss  24381  metcnp3  24496  ngptgp  24592  nrginvrcn  24648  nmoleub  24687  xrsmopn  24769  icccmplem3  24781  reconnlem2  24784  rectbntr0  24789  rescncf  24858  iocopnst  24905  iccpnfcnv  24910  lebnumii  24933  nmoleub2lem  25082  nmhmcn  25088  iscfil3  25241  iscau2  25245  iscau3  25246  iscau4  25247  iscmet3lem2  25260  caussi  25265  equivcfil  25267  equivcau  25268  ivthlem2  25421  ivthlem3  25422  ovoliunlem2  25472  ovoliunnul  25476  ioombl1lem4  25530  dyadmax  25567  dyadmbl  25569  volsup2  25574  itg2le  25708  itg2const2  25710  itg2seq  25711  itgsplitioo  25807  rolle  25962  c1lip1  25970  dvivthlem1  25981  lhop1  25987  dvcnvrelem1  25990  dvfsumrlim  26006  ply1divmo  26109  ig1peu  26148  plypf1  26185  coeaddlem  26222  dvply2g  26260  fta1  26284  quotcan  26285  aalioulem4  26311  ulmcaulem  26371  ulmcn  26376  pilem2  26430  sincosq1lem  26474  sinq12gt0  26484  sinq12ge0  26485  tanord1  26514  lognegb  26567  logrec  26741  logbgcd1irr  26772  dcubic  26824  xrlimcnp  26946  o1cxp  26953  ftalem2  27052  ftalem3  27053  fsumdvdscom  27163  chtub  27191  vmasum  27195  bcmono  27256  bposlem3  27265  bposlem7  27269  lgsdir  27311  lgsqrlem2  27326  lgsqrmodndvds  27332  gausslemma2dlem6  27351  gausslemma2d  27353  lgsquadlem2  27360  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2sqlem6  27402  2sq2  27412  2sqmod  27415  dchrisumlem3  27470  pntrsumbnd2  27546  pntpbnd1  27565  pntibnd  27572  pntlem3  27588  pntleml  27590  ltsres  27642  nosepon  27645  nolesgn2o  27651  nogesgn1o  27653  nodenselem8  27671  nosupbnd1lem1  27688  madess  27874  madebdaylemlrcut  27907  peano5uzs  28412  bdayfinbndlem1  28475  z12bday  28493  brbtwn2  28990  colinearalg  28995  axcontlem10  29058  edgupgr  29219  edglnl  29228  usgruspgrb  29268  subupgr  29372  uhgrspan1  29388  usgredgsscusgredg  29545  fusgrn0degnn0  29585  upgrewlkle2  29692  uspgr2wlkeq  29731  redwlk  29756  wlkdlem2  29767  upgrwlkdvdelem  29821  pthdlem1  29851  pthdlem2  29853  crctcshwlkn0lem3  29897  wlkiswwlks1  29952  wwlksm1edg  29966  wwlksnred  29977  wwlksnextbi  29979  umgr2adedgspth  30033  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a  30085  clwlkclwwlkf1lem3  30093  clwwisshclwwslemlem  30100  clwwlkf  30134  clwwlkext2edg  30143  wwlksubclwwlk  30145  clwwlknonex2lem2  30195  eupth2lems  30325  frgrwopreglem4a  30397  frgrregorufrg  30413  ex-natded5.3-2  30495  isgrpo  30585  vacn  30782  ubthlem2  30959  htthlem  31005  normgt0  31215  shmodsi  31477  spansneleq  31658  h1datomi  31669  nmcexi  32114  pjnormssi  32256  stm1add3i  32335  golem2  32360  cvnsym  32378  dmdmd  32388  mdslmd1lem1  32413  mdslmd1i  32417  mdexchi  32423  atcveq0  32436  superpos  32442  hatomistici  32450  atoml2i  32471  atcvat2i  32475  chirredlem1  32478  atcvat3i  32484  mdsymlem3  32493  mdsymlem5  32495  cdj3lem2b  32525  cdj3i  32529  submarchi  33280  dfufd2  33643  tpr2rico  34090  ordtrest2NEWlem  34100  xrge0iifcnv  34111  omssubadd  34478  eulerpartlemb  34546  ballotlemfc0  34671  ballotlemfcc  34672  ftc2re  34776  fissorduni  35267  fineqvinfep  35303  loop1cycl  35353  subfacp1lem6  35401  iccllysconn  35466  cvmfolem  35495  satfsschain  35580  satfrel  35583  satfdm  35585  sat1el2xp  35595  satffunlem1lem1  35618  dmopab3rexdif  35621  satffunlem2lem2  35622  satffun  35625  fundmpss  35983  dfon2lem3  35999  dfon2lem6  36002  axextbdist  36014  dfrdg4  36167  5segofs  36222  cgrextend  36224  segconeu  36227  btwncomim  36229  btwnswapid  36233  btwnintr  36235  btwnexch3  36236  btwndiff  36243  ifscgr  36260  cgrxfr  36271  btwnxfr  36272  lineext  36292  brofs2  36293  linecgr  36297  lineid  36299  idinside  36300  endofsegid  36301  btwnconn1lem13  36315  btwnconn3  36319  finminlem  36534  nn0prpwlem  36538  cldbnd  36542  clsint2  36545  fnessref  36573  neibastop3  36578  fgmin  36586  onsuct0  36657  limsucncmpi  36661  bj-nnfea  36977  bj-axc14  37104  bj-restn0  37343  bj-0int  37354  wl-19.2reqv  37779  wl-aetr  37784  wl-axc11r  37785  fin2so  37858  tan2h  37863  lindsenlbs  37866  poimirlem2  37873  poimirlem9  37880  poimirlem17  37888  poimirlem18  37889  poimirlem21  37892  poimirlem23  37894  poimirlem26  37897  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  poimir  37904  heicant  37906  mblfinlem2  37909  mblfinlem3  37910  itg2addnclem  37922  itg2addnclem2  37923  itg2gt0cn  37926  ftc1anclem5  37948  ftc1anclem6  37949  filbcmb  37991  nninfnub  38002  mettrifi  38008  geomcau  38010  istotbnd3  38022  sstotbnd2  38025  ismtybndlem  38057  heibor1lem  38060  heiborlem1  38062  heiborlem8  38069  heiborlem10  38071  heibor  38072  opidonOLD  38103  riscer  38239  crngohomfo  38257  keridl  38283  ispridl2  38289  ispridlc  38321  ac6s6  38423  eqvreltr  38942  eldisjdmqsim  39068  suceldisj  39069  eldisjs6  39191  dral1-o  39280  ax12indalem  39321  ax12inda2ALT  39322  lsatcveq0  39408  eqlkr3  39477  atlatmstc  39695  atlrelat1  39697  hlrelat2  39779  intnatN  39783  cvrexchlem  39795  cvratlem  39797  cvrat2  39805  atltcvr  39811  cvrat3  39818  cvrat4  39819  ps-1  39853  ps-2  39854  lplnnle2at  39917  lvolnle3at  39958  2llnma3r  40164  cdlemblem  40169  pmapjoin  40228  elpcliN  40269  lhpmcvr4N  40402  4atexlemnclw  40446  trlnidatb  40553  cdlemc4  40570  cdlemd3  40576  cdleme3g  40610  cdleme7d  40622  cdleme11c  40637  cdleme11dN  40638  cdleme21b  40702  cdleme21c  40703  cdleme21i  40711  cdleme22b  40717  cdleme35fnpq  40825  cdlemf1  40937  trlord  40945  cdlemg6c  40996  dihglblem6  41716  dochlkr  41761  dochkrshp  41762  dihjat1lem  41804  dochexmidlem5  41840  dochexmidlem8  41843  qsalrel  42611  remulcand  42809  prjspner1  42984  fphpdo  43174  pellexlem5  43190  pellexlem6  43191  jm2.26lem3  43358  unxpwdom3  43452  omlimcl2  43599  oe0suclim  43634  cantnfresb  43681  tfsconcatb0  43701  naddgeoa  43751  iscard5  43892  sqrtcval  43997  ov2ssiunov2  44056  frege124d  44117  ordpss  44806  19.41rg  44906  relpfrlem  45309  modelaxreplem2  45335  stoweidlem34  46392  ormklocald  47232  evenwodadd  47245  cfsetsnfsetf1  47419  fcoresf1  47429  euoreqb  47469  2reu8i  47473  ralralimp  47638  f1oresf1o2  47651  zm1nn  47662  elfz2z  47675  2tceilhalfelfzo1  47692  m1modmmod  47718  modlt0b  47723  iccpartlt  47784  iccelpart  47793  icceuelpartlem  47795  fargshiftf1  47801  sprsymrelf1lem  47851  paireqne  47871  reuopreuprim  47886  goldbachthlem2  47906  odz2prm2pw  47923  fmtnoprmfac1lem  47924  fmtnofac2lem  47928  prmdvdsfmtnof1  47947  sfprmdvdsmersenne  47963  lighneallem2  47966  lighneallem4  47970  fppr2odd  48091  gbegt5  48121  gbowge7  48123  bgoldbtbndlem4  48168  bgoldbtbnd  48169  tgoldbach  48177  grimuhgr  48247  grimcnv  48248  grimco  48249  isuspgrim0  48254  isuspgrimlem  48255  upgrimwlklem5  48261  upgrimtrlslem2  48265  uhgrimisgrgriclem  48290  clnbgrgrimlem  48293  clnbgrgrim  48294  grimedg  48295  grtriprop  48301  isubgr3stgrlem3  48328  isubgr3stgrlem4  48329  isubgr3stgrlem6  48331  isubgr3stgrlem7  48332  uspgrlimlem3  48350  grlimedgclnbgr  48355  grlimgrtrilem2  48362  grlimgrtri  48363  grlicsym  48373  gpgedgvtx1  48422  gpgedgiov  48425  gpgedg2ov  48426  gpgedg2iv  48427  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  lcosslsp  48798  lindslinindsimp1  48817  snlindsntor  48831  itcovalt2  49037  eenglngeehlnmlem2  49098  itsclc0yqsol  49124  itschlc0xyqsol1  49126  itschlc0xyqsol  49127  opnneilv  49268  i0oii  49279  io1ii  49280  iscnrm3lem4  49295  iscnrm3r  49307  setrec1lem4  50049  aacllem  50160