Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 29935 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  238  sylbid  239  sylibrd  259  sylbird  260  syland  602  animpimp2impd  843  ax12v2  2172  alrimdd  2206  axc16g  2250  axc16nf  2253  axc11r  2364  sb4a  2478  2eu1  2645  2eu1v  2646  ss2ralv  4052  ss2rexv  4053  trel3  5275  poss  5590  sess2  5645  wefrc  5670  wereu2  5673  predtrss  6323  frpomin  6341  funun  6594  ssimaex  6976  f1cofveqaeq  7260  f1imass  7266  soisoi  7328  isores3  7335  isofrlem  7340  isoselem  7341  weniso  7354  abnexg  7747  oninton  7787  orduniorsuc  7822  limuni3  7845  tfindsg  7854  limom  7875  f1o2ndf1  8113  soxp  8120  xpord3inddlem  8145  soseq  8150  extmptsuppeq  8178  smoel  8366  tfrlem9  8391  tz7.49  8451  seqomlem1  8456  odi  8585  omass  8586  omeulem2  8589  oeordsuc  8600  oeeulem  8607  ertr  8724  swoord2  8741  ecopovtrn  8820  domtriord  9129  pssnn  9174  onomeneqOLD  9235  unxpdomlem2  9257  isinf  9266  isinfOLD  9267  pssnnOLD  9271  f1finf1o  9277  findcard3  9291  findcard3OLD  9292  frfi  9294  unblem3  9303  en3lplem1  9613  inf3lem5  9633  cantnfle  9672  cantnfp1lem3  9681  ttrcltr  9717  frmin  9750  rankxpsuc  9883  tcrank  9885  ficardom  9962  carduni  9982  infxpenlem  10014  dfac8alem  10030  ac10ct  10035  ween  10036  alephdom  10082  alephle  10089  iscard3  10094  alephfp  10109  pwsdompw  10205  infdif  10210  cfslbn  10268  cofsmo  10270  cfcof  10275  fin1a2s  10415  domtriomlem  10443  ac6num  10480  zorn2lem3  10499  axdclem2  10521  imadomg  10535  iundom2g  10541  ficard  10566  fpwwe2lem7  10638  fpwwe2  10644  gchpwdom  10671  gchaclem  10679  tskr1om2  10769  inar1  10776  tskord  10781  tskuni  10784  grudomon  10818  grur1a  10820  grur1  10821  addnidpi  10902  ltexnq  10976  genpnnp  11006  addclprlem2  11018  mulclprlem  11020  psslinpr  11032  ltexprlem6  11042  ltexprlem7  11043  addcanpr  11047  mulgt0sr  11106  map2psrpr  11111  supsrlem  11112  axrrecex  11164  letr  11315  dedekind  11384  recex  11853  lemul12b  12078  mulgt1  12080  fimaxre2  12166  lbreu  12171  nnrecgt0  12262  nnunb  12475  bndndx  12478  zeo  12655  uzind  12661  fzind  12667  fnn0ind  12668  suprfinzcl  12683  suprzcl2  12929  zmax  12936  rpnnen1lem5  12972  xrletr  13144  qbtwnre  13185  qsqueeze  13187  qextltlem  13188  xralrple  13191  xlesubadd  13249  supxrunb1  13305  icoshft  13457  zltaddlt1le  13489  fzen  13525  elfz0fzfz0  13613  elfzmlbp  13619  elfzo0z  13681  fzofzim  13686  fzo1fzo0n0  13690  elfzodifsumelfzo  13705  ssfzoulel  13733  modadd1  13880  modmul1  13896  uzrdgfni  13930  fsuppmapnn0fiub0  13965  fsuppmapnn0ub  13967  fsuppmapnn0fz  13968  seqf1olem1  14014  seqf1olem2  14015  expnbnd  14202  faclbnd4lem4  14263  hashgt23el  14391  seqcoll  14432  hashle2pr  14445  elss2prb  14455  ccatalpha  14550  swrdsbslen  14621  swrdspsleq  14622  swrdswrdlem  14661  swrdswrd  14662  pfxccatin12lem2a  14684  pfxccatin12lem1  14685  pfxccatin12lem3  14689  swrdccat3blem  14696  reuccatpfxs1lem  14703  repswswrd  14741  cshf1  14767  swrd2lsw  14910  sqeqd  15120  sqrmo  15205  cau3lem  15308  icodiamlt  15389  limsupbnd2  15434  lo1bdd2  15475  climuni  15503  rlimcn3  15541  mulcn2  15547  o1of2  15564  rlimo1  15568  lo1le  15605  iseralt  15638  cvgrat  15836  fprodss  15899  rpnnen2lem12  16175  ruclem3  16183  sqrt2irr  16199  p1modz1  16211  dvdsmodexp  16212  dvds2lem  16219  dvdslelem  16259  dvdsabseq  16263  divalglem8  16350  bitsinv1lem  16389  sadcaddlem  16405  smu01lem  16433  smueqlem  16438  bezoutlem4  16491  dfgcd2  16495  algcvga  16523  lcmfunsnlem1  16581  lcmfunsnlem2lem1  16582  lcmfunsnlem2lem2  16583  lcmfdvdsb  16587  coprmgcdb  16593  coprmdvds2  16598  coprmprod  16605  isprm3  16627  prmdvdsfz  16649  isprm5  16651  coprm  16655  rpexp12i  16668  phibndlem  16710  dfphi2  16714  eulerthlem2  16722  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  17547  initoid  17958  termoid  17959  initoeu2lem1  17971  pospo  18305  dirge  18563  cyccom  19122  gsmsymgrfixlem1  19340  oddvdsnn0  19457  oddvds  19460  odcl2  19478  gexdvds  19497  sylow2alem2  19531  sylow2a  19532  efgi2  19638  efgsrel  19647  efgs1b  19649  imasabl  19789  cyggex2  19810  telgsums  19906  pgpfac1lem2  19990  pgpfac1lem3a  19991  pgpfac1lem3  19992  pgpfac1lem5  19994  lmodfopnelem2  20657  lssssr  20712  rnglidlmcl  20986  gzrngunitlem  21214  znunit  21342  frgpcyg  21352  lsmcss  21468  obselocv  21506  obslbs  21508  mhpvarcl  21913  cply1mul  22051  gsummoncoe1  22061  cpmatacl  22451  cpmatinvcl  22452  cpmatmcllem  22453  m2cpminvid2lem  22489  mp2pm2mplem4  22544  pm2mp  22560  chfacfisf  22589  chfacfisfcpmat  22590  chfacfscmul0  22593  chfacfpmmul0  22597  cayhamlem4  22623  ordtrest2lem  22940  leordtval2  22949  lecldbas  22956  cncls  23011  cncnp  23017  cnpresti  23025  lmcnp  23041  cnt0  23083  isreg2  23114  cmpsublem  23136  cmpsub  23137  tgcmp  23138  bwth  23147  dfconn2  23156  1stcfb  23182  1stcelcls  23198  islly2  23221  dislly  23234  reftr  23251  comppfsc  23269  kgencn2  23294  txcnp  23357  txindis  23371  txcmplem1  23378  txlm  23385  xkohaus  23390  cnmptcom  23415  kqfvima  23467  isr0  23474  fgss2  23611  fbasrn  23621  filuni  23622  ufilmax  23644  isufil2  23645  cfinufil  23665  fmfnfmlem1  23691  fmfnfmlem2  23692  fmfnfmlem4  23694  fmfnfm  23695  fmco  23698  flimopn  23712  hausflim  23718  flimrest  23720  fclsopn  23751  flimfnfcls  23765  alexsubALTlem2  23785  alexsubALTlem3  23786  alexsubALT  23788  ptcmplem2  23790  cnextcn  23804  symgtgp  23843  qustgplem  23858  tsmsres  23881  tsmsxplem1  23890  isucn2  24017  imasdsf1olem  24112  bldisj  24137  blssps  24163  blss  24164  metcnp3  24282  ngptgp  24378  nrginvrcn  24442  nmoleub  24481  xrsmopn  24561  icccmplem3  24573  reconnlem2  24576  rectbntr0  24581  rescncf  24650  iocopnst  24697  iccpnfcnv  24702  lebnumii  24725  nmoleub2lem  24874  nmhmcn  24880  iscfil3  25034  iscau2  25038  iscau3  25039  iscau4  25040  iscmet3lem2  25053  caussi  25058  equivcfil  25060  equivcau  25061  ivthlem2  25214  ivthlem3  25215  ovoliunlem2  25265  ovoliunnul  25269  ioombl1lem4  25323  dyadmax  25360  dyadmbl  25362  volsup2  25367  itg2le  25502  itg2const2  25504  itg2seq  25505  itgsplitioo  25600  rolle  25755  c1lip1  25763  dvivthlem1  25774  lhop1  25780  dvcnvrelem1  25783  dvfsumrlim  25797  ply1divmo  25902  ig1peu  25938  plypf1  25975  coeaddlem  26012  fta1  26071  quotcan  26072  aalioulem4  26098  ulmcaulem  26156  ulmcn  26161  pilem2  26215  sincosq1lem  26258  sinq12gt0  26268  sinq12ge0  26269  tanord1  26297  lognegb  26349  logrec  26519  logbgcd1irr  26550  dcubic  26602  xrlimcnp  26724  o1cxp  26730  ftalem2  26829  ftalem3  26830  fsumdvdscom  26940  chtub  26966  vmasum  26970  bcmono  27031  bposlem3  27040  bposlem7  27044  lgsdir  27086  lgsqrlem2  27101  lgsqrmodndvds  27107  gausslemma2dlem6  27126  gausslemma2d  27128  lgsquadlem2  27135  2lgslem3a1  27154  2lgslem3b1  27155  2lgslem3c1  27156  2lgslem3d1  27157  2sqlem6  27177  2sq2  27187  2sqmod  27190  dchrisumlem3  27245  pntrsumbnd2  27321  pntpbnd1  27340  pntibnd  27347  pntlem3  27363  pntleml  27365  sltres  27416  nosepon  27419  nolesgn2o  27425  nogesgn1o  27427  nodenselem8  27445  nosupbnd1lem1  27462  madess  27623  madebdaylemlrcut  27645  brbtwn2  28445  colinearalg  28450  axcontlem10  28513  edgupgr  28676  edglnl  28685  usgruspgrb  28723  subupgr  28826  uhgrspan1  28842  usgredgsscusgredg  28998  fusgrn0degnn0  29038  upgrewlkle2  29145  uspgr2wlkeq  29185  redwlk  29211  wlkdlem2  29222  upgrwlkdvdelem  29275  pthdlem1  29305  pthdlem2  29307  crctcshwlkn0lem3  29348  wlkiswwlks1  29403  wwlksm1edg  29417  wwlksnred  29428  wwlksnextbi  29430  umgr2adedgspth  29484  clwlkclwwlklem2fv2  29531  clwlkclwwlklem2a  29533  clwlkclwwlkf1lem3  29541  clwwisshclwwslemlem  29548  clwwlkf  29582  clwwlkext2edg  29591  wwlksubclwwlk  29593  clwwlknonex2lem2  29643  eupth2lems  29773  frgrwopreglem4a  29845  frgrregorufrg  29861  ex-natded5.3-2  29943  isgrpo  30032  vacn  30229  ubthlem2  30406  htthlem  30452  normgt0  30662  shmodsi  30924  spansneleq  31105  h1datomi  31116  nmcexi  31561  pjnormssi  31703  stm1add3i  31782  golem2  31807  cvnsym  31825  dmdmd  31835  mdslmd1lem1  31860  mdslmd1i  31864  mdexchi  31870  atcveq0  31883  superpos  31889  hatomistici  31897  atoml2i  31918  atcvat2i  31922  chirredlem1  31925  atcvat3i  31931  mdsymlem3  31940  mdsymlem5  31942  cdj3lem2b  31972  cdj3i  31976  supssd  32216  infssd  32217  resspos  32418  resstos  32419  submarchi  32617  tpr2rico  33205  ordtrest2NEWlem  33215  xrge0iifcnv  33226  omssubadd  33612  eulerpartlemb  33680  ballotlemfc0  33804  ballotlemfcc  33805  ftc2re  33923  loop1cycl  34441  subfacp1lem6  34489  iccllysconn  34554  cvmfolem  34583  satfsschain  34668  satfrel  34671  satfdm  34673  sat1el2xp  34683  satffunlem1lem1  34706  dmopab3rexdif  34709  satffunlem2lem2  34710  satffun  34713  fundmpss  35057  dfon2lem3  35076  dfon2lem6  35079  axextbdist  35091  dfrdg4  35242  5segofs  35297  cgrextend  35299  segconeu  35302  btwncomim  35304  btwnswapid  35308  btwnintr  35310  btwnexch3  35311  btwndiff  35318  ifscgr  35335  cgrxfr  35346  btwnxfr  35347  lineext  35367  brofs2  35368  linecgr  35372  lineid  35374  idinside  35375  endofsegid  35376  btwnconn1lem13  35390  btwnconn3  35394  finminlem  35519  nn0prpwlem  35523  cldbnd  35527  clsint2  35530  fnessref  35558  neibastop3  35563  fgmin  35571  onsuct0  35642  limsucncmpi  35646  bj-nnfea  35928  bj-axc14  36051  bj-restn0  36287  bj-0int  36298  wl-19.2reqv  36709  wl-aetr  36714  wl-axc11r  36715  fin2so  36791  tan2h  36796  lindsenlbs  36799  poimirlem2  36806  poimirlem9  36813  poimirlem17  36821  poimirlem18  36822  poimirlem21  36825  poimirlem23  36827  poimirlem26  36830  poimirlem29  36833  poimirlem30  36834  poimirlem31  36835  poimir  36837  heicant  36839  mblfinlem2  36842  mblfinlem3  36843  itg2addnclem  36855  itg2addnclem2  36856  itg2gt0cn  36859  ftc1anclem5  36881  ftc1anclem6  36882  filbcmb  36924  nninfnub  36935  mettrifi  36941  geomcau  36943  istotbnd3  36955  sstotbnd2  36958  ismtybndlem  36990  heibor1lem  36993  heiborlem1  36995  heiborlem8  37002  heiborlem10  37004  heibor  37005  opidonOLD  37036  riscer  37172  crngohomfo  37190  keridl  37216  ispridl2  37222  ispridlc  37254  ac6s6  37356  eqvreltr  37793  dral1-o  38090  ax12indalem  38131  ax12inda2ALT  38132  lsatcveq0  38218  eqlkr3  38287  atlatmstc  38505  atlrelat1  38507  hlrelat2  38590  intnatN  38594  cvrexchlem  38606  cvratlem  38608  cvrat2  38616  atltcvr  38622  cvrat3  38629  cvrat4  38630  ps-1  38664  ps-2  38665  lplnnle2at  38728  lvolnle3at  38769  2llnma3r  38975  cdlemblem  38980  pmapjoin  39039  elpcliN  39080  lhpmcvr4N  39213  4atexlemnclw  39257  trlnidatb  39364  cdlemc4  39381  cdlemd3  39387  cdleme3g  39421  cdleme7d  39433  cdleme11c  39448  cdleme11dN  39449  cdleme21b  39513  cdleme21c  39514  cdleme21i  39522  cdleme22b  39528  cdleme35fnpq  39636  cdlemf1  39748  trlord  39756  cdlemg6c  39807  dihglblem6  40527  dochlkr  40572  dochkrshp  40573  dihjat1lem  40615  dochexmidlem5  40651  dochexmidlem8  40654  metakunt29  41332  qsalrel  41381  remulcand  41626  prjspner1  41683  fphpdo  41870  pellexlem5  41886  pellexlem6  41887  jm2.26lem3  42055  unxpwdom3  42152  omlimcl2  42306  oe0suclim  42342  cantnfresb  42389  tfsconcatb0  42409  naddsuc2  42458  naddgeoa  42460  iscard5  42602  sqrtcval  42707  ov2ssiunov2  42766  frege124d  42827  ordpss  43525  19.41rg  43626  stoweidlem34  45061  cfsetsnfsetf1  46080  fcoresf1  46090  euoreqb  46128  2reu8i  46132  ralralimp  46297  f1oresf1o2  46310  zm1nn  46321  elfz2z  46334  iccpartlt  46403  iccelpart  46412  icceuelpartlem  46414  fargshiftf1  46420  sprsymrelf1lem  46470  paireqne  46490  reuopreuprim  46505  goldbachthlem2  46525  odz2prm2pw  46542  fmtnoprmfac1lem  46543  fmtnofac2lem  46547  prmdvdsfmtnof1  46566  sfprmdvdsmersenne  46582  lighneallem2  46585  lighneallem4  46589  fppr2odd  46710  gbegt5  46740  gbowge7  46742  bgoldbtbndlem4  46787  bgoldbtbnd  46788  tgoldbach  46796  isomuspgrlem2b  46808  isomgrsym  46815  zrtermorngc  47000  zrtermoringc  47069  lcosslsp  47219  lindslinindsimp1  47238  snlindsntor  47252  m1modmmod  47307  itcovalt2  47463  eenglngeehlnmlem2  47524  itsclc0yqsol  47550  itschlc0xyqsol1  47552  itschlc0xyqsol  47553  opnneilv  47641  i0oii  47652  io1ii  47653  iscnrm3lem4  47669  iscnrm3r  47681  setrec1lem4  47835  aacllem  47948