Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30366 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  4036  ss2rexv  4037  trel3  5251  poss  5576  sess2  5633  wefrc  5661  wereu2  5664  predtrss  6324  frpomin  6342  funun  6593  ssimaex  6975  f1cofveqaeq  7261  f1imass  7267  soisoi  7331  isores3  7338  isofrlem  7343  isoselem  7344  weniso  7357  abnexg  7759  oninton  7798  orduniorsuc  7833  limuni3  7856  tfindsg  7865  limom  7886  resf1extb  7939  f1o2ndf1  8130  soxp  8137  xpord3inddlem  8162  soseq  8167  extmptsuppeq  8196  smoel  8383  tfrlem9  8408  tz7.49  8468  seqomlem1  8473  odi  8600  omass  8601  omeulem2  8604  oeordsuc  8615  oeeulem  8622  naddsuc2  8722  ertr  8743  swoord2  8761  ecopovtrn  8843  domtriord  9146  pssnn  9191  onomeneqOLD  9249  unxpdomlem2  9270  isinf  9279  isinfOLD  9280  f1finf1o  9288  findcard3  9301  findcard3OLD  9302  frfi  9304  unblem3  9313  en3lplem1  9635  inf3lem5  9655  cantnfle  9694  cantnfp1lem3  9703  ttrcltr  9739  frmin  9772  rankxpsuc  9905  tcrank  9907  ficardom  9984  carduni  10004  infxpenlem  10036  dfac8alem  10052  ac10ct  10057  ween  10058  alephdom  10104  alephle  10111  iscard3  10116  alephfp  10131  pwsdompw  10226  infdif  10231  cfslbn  10290  cofsmo  10292  cfcof  10297  fin1a2s  10437  domtriomlem  10465  ac6num  10502  zorn2lem3  10521  axdclem2  10543  imadomg  10557  iundom2g  10563  ficard  10588  fpwwe2lem7  10660  fpwwe2  10666  gchpwdom  10693  gchaclem  10701  tskr1om2  10791  inar1  10798  tskord  10803  tskuni  10806  grudomon  10840  grur1a  10842  grur1  10843  addnidpi  10924  ltexnq  10998  genpnnp  11028  addclprlem2  11040  mulclprlem  11042  psslinpr  11054  ltexprlem6  11064  ltexprlem7  11065  addcanpr  11069  mulgt0sr  11128  map2psrpr  11133  supsrlem  11134  axrrecex  11186  letr  11338  dedekind  11407  recex  11878  lemul12b  12107  mulgt1OLD  12109  fimaxre2  12196  lbreu  12201  nnrecgt0  12292  nnunb  12506  bndndx  12509  zeo  12688  uzind  12694  fzind  12700  fnn0ind  12701  suprfinzcl  12716  suprzcl2  12963  zmax  12970  rpnnen1lem5  13006  xrletr  13183  qbtwnre  13224  qsqueeze  13226  qextltlem  13227  xralrple  13230  xlesubadd  13288  supxrunb1  13344  icoshft  13496  zltaddlt1le  13528  fzen  13564  elfz0fzfz0  13656  elfzmlbp  13662  elfzo0z  13724  fzofzim  13732  fzo1fzo0n0  13737  elfzodifsumelfzo  13753  ssfzoulel  13782  modadd1  13931  modmul1  13948  uzrdgfni  13982  fsuppmapnn0fiub0  14017  fsuppmapnn0ub  14019  fsuppmapnn0fz  14020  seqf1olem1  14065  seqf1olem2  14066  expnbnd  14254  faclbnd4lem4  14318  hashgt23el  14446  seqcoll  14486  hashle2pr  14499  elss2prb  14510  ccatalpha  14614  swrdsbslen  14685  swrdspsleq  14686  swrdswrdlem  14725  swrdswrd  14726  pfxccatin12lem2a  14748  pfxccatin12lem1  14749  pfxccatin12lem3  14753  swrdccat3blem  14760  reuccatpfxs1lem  14767  repswswrd  14805  cshf1  14831  swrd2lsw  14974  sqeqd  15188  sqrmo  15273  cau3lem  15376  icodiamlt  15457  limsupbnd2  15502  lo1bdd2  15543  climuni  15571  rlimcn3  15609  mulcn2  15615  o1of2  15632  rlimo1  15636  lo1le  15671  iseralt  15704  cvgrat  15902  fprodss  15967  rpnnen2lem12  16244  ruclem3  16252  sqrt2irr  16268  p1modz1  16280  dvdsmodexp  16281  dvds2lem  16289  dvdslelem  16329  dvdsabseq  16333  divalglem8  16420  bitsinv1lem  16461  sadcaddlem  16477  smu01lem  16505  smueqlem  16510  bezoutlem4  16562  dfgcd2  16566  algcvga  16599  lcmfunsnlem1  16657  lcmfunsnlem2lem1  16658  lcmfunsnlem2lem2  16659  lcmfdvdsb  16663  coprmgcdb  16669  coprmdvds2  16674  coprmprod  16681  isprm3  16703  prmdvdsfz  16725  isprm5  16727  coprm  16731  rpexp12i  16744  phibndlem  16790  dfphi2  16794  eulerthlem2  16802  odzdvds  16816  iserodd  16856  pclem  16859  pcpremul  16864  pcqcl  16877  pcdvdsb  16890  pcprmpw2  16903  difsqpwdvds  16908  pcaddlem  16909  pcmptcl  16912  pcfac  16920  prmpwdvds  16925  unbenlem  16929  prmreclem1  16937  4sqlem17  16982  vdwmc2  17000  vdwlem9  17010  vdwlem10  17011  vdwlem13  17014  vdwnnlem3  17018  ramcl  17050  prmgaplem7  17078  mreiincl  17615  initoid  18022  termoid  18023  initoeu2lem1  18035  pospo  18364  dirge  18622  cyccom  19195  gsmsymgrfixlem1  19418  oddvdsnn0  19535  oddvds  19538  odcl2  19556  gexdvds  19575  sylow2alem2  19609  sylow2a  19610  efgi2  19716  efgsrel  19725  efgs1b  19727  imasabl  19867  cyggex2  19888  telgsums  19984  pgpfac1lem2  20068  pgpfac1lem3a  20069  pgpfac1lem3  20070  pgpfac1lem5  20072  zrtermorngc  20616  zrtermoringc  20648  lmodfopnelem2  20870  lssssr  20925  rnglidlmcl  21193  gzrngunitlem  21417  znunit  21549  frgpcyg  21559  lsmcss  21677  obselocv  21715  obslbs  21717  mhpvarcl  22119  cply1mul  22267  gsummoncoe1  22279  cpmatacl  22689  cpmatinvcl  22690  cpmatmcllem  22691  m2cpminvid2lem  22727  mp2pm2mplem4  22782  pm2mp  22798  chfacfisf  22827  chfacfisfcpmat  22828  chfacfscmul0  22831  chfacfpmmul0  22835  cayhamlem4  22861  ordtrest2lem  23176  leordtval2  23185  lecldbas  23192  cncls  23247  cncnp  23253  cnpresti  23261  lmcnp  23277  cnt0  23319  isreg2  23350  cmpsublem  23372  cmpsub  23373  tgcmp  23374  bwth  23383  dfconn2  23392  1stcfb  23418  1stcelcls  23434  islly2  23457  dislly  23470  reftr  23487  comppfsc  23505  kgencn2  23530  txcnp  23593  txindis  23607  txcmplem1  23614  txlm  23621  xkohaus  23626  cnmptcom  23651  kqfvima  23703  isr0  23710  fgss2  23847  fbasrn  23857  filuni  23858  ufilmax  23880  isufil2  23881  cfinufil  23901  fmfnfmlem1  23927  fmfnfmlem2  23928  fmfnfmlem4  23930  fmfnfm  23931  fmco  23934  flimopn  23948  hausflim  23954  flimrest  23956  fclsopn  23987  flimfnfcls  24001  alexsubALTlem2  24021  alexsubALTlem3  24022  alexsubALT  24024  ptcmplem2  24026  cnextcn  24040  symgtgp  24079  qustgplem  24094  tsmsres  24117  tsmsxplem1  24126  isucn2  24252  imasdsf1olem  24347  bldisj  24372  blssps  24398  blss  24399  metcnp3  24516  ngptgp  24612  nrginvrcn  24668  nmoleub  24707  xrsmopn  24789  icccmplem3  24801  reconnlem2  24804  rectbntr0  24809  rescncf  24878  iocopnst  24925  iccpnfcnv  24930  lebnumii  24953  nmoleub2lem  25102  nmhmcn  25108  iscfil3  25262  iscau2  25266  iscau3  25267  iscau4  25268  iscmet3lem2  25281  caussi  25286  equivcfil  25288  equivcau  25289  ivthlem2  25442  ivthlem3  25443  ovoliunlem2  25493  ovoliunnul  25497  ioombl1lem4  25551  dyadmax  25588  dyadmbl  25590  volsup2  25595  itg2le  25729  itg2const2  25731  itg2seq  25732  itgsplitioo  25828  rolle  25983  c1lip1  25991  dvivthlem1  26002  lhop1  26008  dvcnvrelem1  26011  dvfsumrlim  26027  ply1divmo  26130  ig1peu  26169  plypf1  26206  coeaddlem  26243  dvply2g  26281  fta1  26305  quotcan  26306  aalioulem4  26332  ulmcaulem  26392  ulmcn  26397  pilem2  26451  sincosq1lem  26494  sinq12gt0  26504  sinq12ge0  26505  tanord1  26534  lognegb  26587  logrec  26761  logbgcd1irr  26792  dcubic  26844  xrlimcnp  26966  o1cxp  26973  ftalem2  27072  ftalem3  27073  fsumdvdscom  27183  chtub  27211  vmasum  27215  bcmono  27276  bposlem3  27285  bposlem7  27289  lgsdir  27331  lgsqrlem2  27346  lgsqrmodndvds  27352  gausslemma2dlem6  27371  gausslemma2d  27373  lgsquadlem2  27380  2lgslem3a1  27399  2lgslem3b1  27400  2lgslem3c1  27401  2lgslem3d1  27402  2sqlem6  27422  2sq2  27432  2sqmod  27435  dchrisumlem3  27490  pntrsumbnd2  27566  pntpbnd1  27585  pntibnd  27592  pntlem3  27608  pntleml  27610  sltres  27662  nosepon  27665  nolesgn2o  27671  nogesgn1o  27673  nodenselem8  27691  nosupbnd1lem1  27708  madess  27870  madebdaylemlrcut  27892  peano5uzs  28345  brbtwn2  28869  colinearalg  28874  axcontlem10  28937  edgupgr  29098  edglnl  29107  usgruspgrb  29147  subupgr  29251  uhgrspan1  29267  usgredgsscusgredg  29424  fusgrn0degnn0  29464  upgrewlkle2  29571  uspgr2wlkeq  29611  redwlk  29637  wlkdlem2  29648  upgrwlkdvdelem  29703  pthdlem1  29733  pthdlem2  29735  crctcshwlkn0lem3  29779  wlkiswwlks1  29834  wwlksm1edg  29848  wwlksnred  29859  wwlksnextbi  29861  umgr2adedgspth  29915  clwlkclwwlklem2fv2  29962  clwlkclwwlklem2a  29964  clwlkclwwlkf1lem3  29972  clwwisshclwwslemlem  29979  clwwlkf  30013  clwwlkext2edg  30022  wwlksubclwwlk  30024  clwwlknonex2lem2  30074  eupth2lems  30204  frgrwopreglem4a  30276  frgrregorufrg  30292  ex-natded5.3-2  30374  isgrpo  30463  vacn  30660  ubthlem2  30837  htthlem  30883  normgt0  31093  shmodsi  31355  spansneleq  31536  h1datomi  31547  nmcexi  31992  pjnormssi  32134  stm1add3i  32213  golem2  32238  cvnsym  32256  dmdmd  32266  mdslmd1lem1  32291  mdslmd1i  32295  mdexchi  32301  atcveq0  32314  superpos  32320  hatomistici  32328  atoml2i  32349  atcvat2i  32353  chirredlem1  32356  atcvat3i  32362  mdsymlem3  32371  mdsymlem5  32373  cdj3lem2b  32403  cdj3i  32407  supssd  32668  infssd  32669  resspos  32902  resstos  32903  submarchi  33139  dfufd2  33519  tpr2rico  33852  ordtrest2NEWlem  33862  xrge0iifcnv  33873  omssubadd  34243  eulerpartlemb  34311  ballotlemfc0  34436  ballotlemfcc  34437  ftc2re  34554  loop1cycl  35083  subfacp1lem6  35131  iccllysconn  35196  cvmfolem  35225  satfsschain  35310  satfrel  35313  satfdm  35315  sat1el2xp  35325  satffunlem1lem1  35348  dmopab3rexdif  35351  satffunlem2lem2  35352  satffun  35355  fundmpss  35708  dfon2lem3  35727  dfon2lem6  35730  axextbdist  35742  dfrdg4  35893  5segofs  35948  cgrextend  35950  segconeu  35953  btwncomim  35955  btwnswapid  35959  btwnintr  35961  btwnexch3  35962  btwndiff  35969  ifscgr  35986  cgrxfr  35997  btwnxfr  35998  lineext  36018  brofs2  36019  linecgr  36023  lineid  36025  idinside  36026  endofsegid  36027  btwnconn1lem13  36041  btwnconn3  36045  finminlem  36260  nn0prpwlem  36264  cldbnd  36268  clsint2  36271  fnessref  36299  neibastop3  36304  fgmin  36312  onsuct0  36383  limsucncmpi  36387  bj-nnfea  36676  bj-axc14  36798  bj-restn0  37032  bj-0int  37043  wl-19.2reqv  37466  wl-aetr  37471  wl-axc11r  37472  fin2so  37555  tan2h  37560  lindsenlbs  37563  poimirlem2  37570  poimirlem9  37577  poimirlem17  37585  poimirlem18  37586  poimirlem21  37589  poimirlem23  37591  poimirlem26  37594  poimirlem29  37597  poimirlem30  37598  poimirlem31  37599  poimir  37601  heicant  37603  mblfinlem2  37606  mblfinlem3  37607  itg2addnclem  37619  itg2addnclem2  37620  itg2gt0cn  37623  ftc1anclem5  37645  ftc1anclem6  37646  filbcmb  37688  nninfnub  37699  mettrifi  37705  geomcau  37707  istotbnd3  37719  sstotbnd2  37722  ismtybndlem  37754  heibor1lem  37757  heiborlem1  37759  heiborlem8  37766  heiborlem10  37768  heibor  37769  opidonOLD  37800  riscer  37936  crngohomfo  37954  keridl  37980  ispridl2  37986  ispridlc  38018  ac6s6  38120  eqvreltr  38549  dral1-o  38846  ax12indalem  38887  ax12inda2ALT  38888  lsatcveq0  38974  eqlkr3  39043  atlatmstc  39261  atlrelat1  39263  hlrelat2  39346  intnatN  39350  cvrexchlem  39362  cvratlem  39364  cvrat2  39372  atltcvr  39378  cvrat3  39385  cvrat4  39386  ps-1  39420  ps-2  39421  lplnnle2at  39484  lvolnle3at  39525  2llnma3r  39731  cdlemblem  39736  pmapjoin  39795  elpcliN  39836  lhpmcvr4N  39969  4atexlemnclw  40013  trlnidatb  40120  cdlemc4  40137  cdlemd3  40143  cdleme3g  40177  cdleme7d  40189  cdleme11c  40204  cdleme11dN  40205  cdleme21b  40269  cdleme21c  40270  cdleme21i  40278  cdleme22b  40284  cdleme35fnpq  40392  cdlemf1  40504  trlord  40512  cdlemg6c  40563  dihglblem6  41283  dochlkr  41328  dochkrshp  41329  dihjat1lem  41371  dochexmidlem5  41407  dochexmidlem8  41410  metakunt29  42175  qsalrel  42221  remulcand  42413  prjspner1  42581  fphpdo  42773  pellexlem5  42789  pellexlem6  42790  jm2.26lem3  42958  unxpwdom3  43052  omlimcl2  43199  oe0suclim  43235  cantnfresb  43282  tfsconcatb0  43302  naddgeoa  43352  iscard5  43494  sqrtcval  43599  ov2ssiunov2  43658  frege124d  43719  ordpss  44415  19.41rg  44515  relpfrlem  44919  modelaxreplem2  44941  stoweidlem34  45994  ormklocald  46834  evenwodadd  46848  cfsetsnfsetf1  47017  fcoresf1  47027  euoreqb  47067  2reu8i  47071  ralralimp  47236  f1oresf1o2  47249  zm1nn  47260  elfz2z  47273  iccpartlt  47357  iccelpart  47366  icceuelpartlem  47368  fargshiftf1  47374  sprsymrelf1lem  47424  paireqne  47444  reuopreuprim  47459  goldbachthlem2  47479  odz2prm2pw  47496  fmtnoprmfac1lem  47497  fmtnofac2lem  47501  prmdvdsfmtnof1  47520  sfprmdvdsmersenne  47536  lighneallem2  47539  lighneallem4  47543  fppr2odd  47664  gbegt5  47694  gbowge7  47696  bgoldbtbndlem4  47741  bgoldbtbnd  47742  tgoldbach  47750  isuspgrim0  47818  isuspgrimlem  47820  grimuhgr  47824  grimcnv  47825  grimco  47826  uhgrimisgrgriclem  47844  clnbgrgrimlem  47847  clnbgrgrim  47848  grimedg  47849  grtriprop  47854  isubgr3stgrlem3  47881  isubgr3stgrlem4  47882  isubgr3stgrlem6  47884  isubgr3stgrlem7  47885  uspgrlimlem3  47903  grlimgrtrilem2  47908  grlimgrtri  47909  grlicsym  47919  2tceilhalfelfzo1  47964  gpgedgvtx1  47966  lcosslsp  48301  lindslinindsimp1  48320  snlindsntor  48334  m1modmmod  48388  itcovalt2  48544  eenglngeehlnmlem2  48605  itsclc0yqsol  48631  itschlc0xyqsol1  48633  itschlc0xyqsol  48634  opnneilv  48754  i0oii  48765  io1ii  48766  iscnrm3lem4  48781  iscnrm3r  48793  setrec1lem4  49205  aacllem  49316