Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30432 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  602  animpimp2impd  845  ax12v2  2180  alrimdd  2215  axc16g  2261  axc16nf  2264  axc11r  2374  sb4a  2488  2eu1  2654  2eu1v  2655  ss2ralv  4079  ss2rexv  4080  trel3  5293  poss  5609  sess2  5666  wefrc  5694  wereu2  5697  predtrss  6354  frpomin  6372  funun  6624  ssimaex  7007  f1cofveqaeq  7295  f1imass  7301  soisoi  7364  isores3  7371  isofrlem  7376  isoselem  7377  weniso  7390  abnexg  7791  oninton  7831  orduniorsuc  7866  limuni3  7889  tfindsg  7898  limom  7919  f1o2ndf1  8163  soxp  8170  xpord3inddlem  8195  soseq  8200  extmptsuppeq  8229  smoel  8416  tfrlem9  8441  tz7.49  8501  seqomlem1  8506  odi  8635  omass  8636  omeulem2  8639  oeordsuc  8650  oeeulem  8657  naddsuc2  8757  ertr  8778  swoord2  8796  ecopovtrn  8878  domtriord  9189  pssnn  9234  onomeneqOLD  9292  unxpdomlem2  9314  isinf  9323  isinfOLD  9324  f1finf1o  9333  findcard3  9346  findcard3OLD  9347  frfi  9349  unblem3  9358  en3lplem1  9681  inf3lem5  9701  cantnfle  9740  cantnfp1lem3  9749  ttrcltr  9785  frmin  9818  rankxpsuc  9951  tcrank  9953  ficardom  10030  carduni  10050  infxpenlem  10082  dfac8alem  10098  ac10ct  10103  ween  10104  alephdom  10150  alephle  10157  iscard3  10162  alephfp  10177  pwsdompw  10272  infdif  10277  cfslbn  10336  cofsmo  10338  cfcof  10343  fin1a2s  10483  domtriomlem  10511  ac6num  10548  zorn2lem3  10567  axdclem2  10589  imadomg  10603  iundom2g  10609  ficard  10634  fpwwe2lem7  10706  fpwwe2  10712  gchpwdom  10739  gchaclem  10747  tskr1om2  10837  inar1  10844  tskord  10849  tskuni  10852  grudomon  10886  grur1a  10888  grur1  10889  addnidpi  10970  ltexnq  11044  genpnnp  11074  addclprlem2  11086  mulclprlem  11088  psslinpr  11100  ltexprlem6  11110  ltexprlem7  11111  addcanpr  11115  mulgt0sr  11174  map2psrpr  11179  supsrlem  11180  axrrecex  11232  letr  11384  dedekind  11453  recex  11922  lemul12b  12151  mulgt1OLD  12153  fimaxre2  12240  lbreu  12245  nnrecgt0  12336  nnunb  12549  bndndx  12552  zeo  12729  uzind  12735  fzind  12741  fnn0ind  12742  suprfinzcl  12757  suprzcl2  13003  zmax  13010  rpnnen1lem5  13046  xrletr  13220  qbtwnre  13261  qsqueeze  13263  qextltlem  13264  xralrple  13267  xlesubadd  13325  supxrunb1  13381  icoshft  13533  zltaddlt1le  13565  fzen  13601  elfz0fzfz0  13690  elfzmlbp  13696  elfzo0z  13758  fzofzim  13763  fzo1fzo0n0  13767  elfzodifsumelfzo  13782  ssfzoulel  13810  modadd1  13959  modmul1  13975  uzrdgfni  14009  fsuppmapnn0fiub0  14044  fsuppmapnn0ub  14046  fsuppmapnn0fz  14047  seqf1olem1  14092  seqf1olem2  14093  expnbnd  14281  faclbnd4lem4  14345  hashgt23el  14473  seqcoll  14513  hashle2pr  14526  elss2prb  14537  ccatalpha  14641  swrdsbslen  14712  swrdspsleq  14713  swrdswrdlem  14752  swrdswrd  14753  pfxccatin12lem2a  14775  pfxccatin12lem1  14776  pfxccatin12lem3  14780  swrdccat3blem  14787  reuccatpfxs1lem  14794  repswswrd  14832  cshf1  14858  swrd2lsw  15001  sqeqd  15215  sqrmo  15300  cau3lem  15403  icodiamlt  15484  limsupbnd2  15529  lo1bdd2  15570  climuni  15598  rlimcn3  15636  mulcn2  15642  o1of2  15659  rlimo1  15663  lo1le  15700  iseralt  15733  cvgrat  15931  fprodss  15996  rpnnen2lem12  16273  ruclem3  16281  sqrt2irr  16297  p1modz1  16309  dvdsmodexp  16310  dvds2lem  16317  dvdslelem  16357  dvdsabseq  16361  divalglem8  16448  bitsinv1lem  16487  sadcaddlem  16503  smu01lem  16531  smueqlem  16536  bezoutlem4  16589  dfgcd2  16593  algcvga  16626  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfdvdsb  16690  coprmgcdb  16696  coprmdvds2  16701  coprmprod  16708  isprm3  16730  prmdvdsfz  16752  isprm5  16754  coprm  16758  rpexp12i  16771  phibndlem  16817  dfphi2  16821  eulerthlem2  16829  odzdvds  16842  iserodd  16882  pclem  16885  pcpremul  16890  pcqcl  16903  pcdvdsb  16916  pcprmpw2  16929  difsqpwdvds  16934  pcaddlem  16935  pcmptcl  16938  pcfac  16946  prmpwdvds  16951  unbenlem  16955  prmreclem1  16963  4sqlem17  17008  vdwmc2  17026  vdwlem9  17036  vdwlem10  17037  vdwlem13  17040  vdwnnlem3  17044  ramcl  17076  prmgaplem7  17104  mreiincl  17654  initoid  18068  termoid  18069  initoeu2lem1  18081  pospo  18415  dirge  18673  cyccom  19243  gsmsymgrfixlem1  19469  oddvdsnn0  19586  oddvds  19589  odcl2  19607  gexdvds  19626  sylow2alem2  19660  sylow2a  19661  efgi2  19767  efgsrel  19776  efgs1b  19778  imasabl  19918  cyggex2  19939  telgsums  20035  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem5  20123  zrtermorngc  20665  zrtermoringc  20697  lmodfopnelem2  20919  lssssr  20975  rnglidlmcl  21249  gzrngunitlem  21473  znunit  21605  frgpcyg  21615  lsmcss  21733  obselocv  21771  obslbs  21773  mhpvarcl  22175  cply1mul  22321  gsummoncoe1  22333  cpmatacl  22743  cpmatinvcl  22744  cpmatmcllem  22745  m2cpminvid2lem  22781  mp2pm2mplem4  22836  pm2mp  22852  chfacfisf  22881  chfacfisfcpmat  22882  chfacfscmul0  22885  chfacfpmmul0  22889  cayhamlem4  22915  ordtrest2lem  23232  leordtval2  23241  lecldbas  23248  cncls  23303  cncnp  23309  cnpresti  23317  lmcnp  23333  cnt0  23375  isreg2  23406  cmpsublem  23428  cmpsub  23429  tgcmp  23430  bwth  23439  dfconn2  23448  1stcfb  23474  1stcelcls  23490  islly2  23513  dislly  23526  reftr  23543  comppfsc  23561  kgencn2  23586  txcnp  23649  txindis  23663  txcmplem1  23670  txlm  23677  xkohaus  23682  cnmptcom  23707  kqfvima  23759  isr0  23766  fgss2  23903  fbasrn  23913  filuni  23914  ufilmax  23936  isufil2  23937  cfinufil  23957  fmfnfmlem1  23983  fmfnfmlem2  23984  fmfnfmlem4  23986  fmfnfm  23987  fmco  23990  flimopn  24004  hausflim  24010  flimrest  24012  fclsopn  24043  flimfnfcls  24057  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALT  24080  ptcmplem2  24082  cnextcn  24096  symgtgp  24135  qustgplem  24150  tsmsres  24173  tsmsxplem1  24182  isucn2  24309  imasdsf1olem  24404  bldisj  24429  blssps  24455  blss  24456  metcnp3  24574  ngptgp  24670  nrginvrcn  24734  nmoleub  24773  xrsmopn  24853  icccmplem3  24865  reconnlem2  24868  rectbntr0  24873  rescncf  24942  iocopnst  24989  iccpnfcnv  24994  lebnumii  25017  nmoleub2lem  25166  nmhmcn  25172  iscfil3  25326  iscau2  25330  iscau3  25331  iscau4  25332  iscmet3lem2  25345  caussi  25350  equivcfil  25352  equivcau  25353  ivthlem2  25506  ivthlem3  25507  ovoliunlem2  25557  ovoliunnul  25561  ioombl1lem4  25615  dyadmax  25652  dyadmbl  25654  volsup2  25659  itg2le  25794  itg2const2  25796  itg2seq  25797  itgsplitioo  25893  rolle  26048  c1lip1  26056  dvivthlem1  26067  lhop1  26073  dvcnvrelem1  26076  dvfsumrlim  26092  ply1divmo  26195  ig1peu  26234  plypf1  26271  coeaddlem  26308  dvply2g  26344  fta1  26368  quotcan  26369  aalioulem4  26395  ulmcaulem  26455  ulmcn  26460  pilem2  26514  sincosq1lem  26557  sinq12gt0  26567  sinq12ge0  26568  tanord1  26597  lognegb  26650  logrec  26824  logbgcd1irr  26855  dcubic  26907  xrlimcnp  27029  o1cxp  27036  ftalem2  27135  ftalem3  27136  fsumdvdscom  27246  chtub  27274  vmasum  27278  bcmono  27339  bposlem3  27348  bposlem7  27352  lgsdir  27394  lgsqrlem2  27409  lgsqrmodndvds  27415  gausslemma2dlem6  27434  gausslemma2d  27436  lgsquadlem2  27443  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  2sqlem6  27485  2sq2  27495  2sqmod  27498  dchrisumlem3  27553  pntrsumbnd2  27629  pntpbnd1  27648  pntibnd  27655  pntlem3  27671  pntleml  27673  sltres  27725  nosepon  27728  nolesgn2o  27734  nogesgn1o  27736  nodenselem8  27754  nosupbnd1lem1  27771  madess  27933  madebdaylemlrcut  27955  peano5uzs  28408  brbtwn2  28938  colinearalg  28943  axcontlem10  29006  edgupgr  29169  edglnl  29178  usgruspgrb  29218  subupgr  29322  uhgrspan1  29338  usgredgsscusgredg  29495  fusgrn0degnn0  29535  upgrewlkle2  29642  uspgr2wlkeq  29682  redwlk  29708  wlkdlem2  29719  upgrwlkdvdelem  29772  pthdlem1  29802  pthdlem2  29804  crctcshwlkn0lem3  29845  wlkiswwlks1  29900  wwlksm1edg  29914  wwlksnred  29925  wwlksnextbi  29927  umgr2adedgspth  29981  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a  30030  clwlkclwwlkf1lem3  30038  clwwisshclwwslemlem  30045  clwwlkf  30079  clwwlkext2edg  30088  wwlksubclwwlk  30090  clwwlknonex2lem2  30140  eupth2lems  30270  frgrwopreglem4a  30342  frgrregorufrg  30358  ex-natded5.3-2  30440  isgrpo  30529  vacn  30726  ubthlem2  30903  htthlem  30949  normgt0  31159  shmodsi  31421  spansneleq  31602  h1datomi  31613  nmcexi  32058  pjnormssi  32200  stm1add3i  32279  golem2  32304  cvnsym  32322  dmdmd  32332  mdslmd1lem1  32357  mdslmd1i  32361  mdexchi  32367  atcveq0  32380  superpos  32386  hatomistici  32394  atoml2i  32415  atcvat2i  32419  chirredlem1  32422  atcvat3i  32428  mdsymlem3  32437  mdsymlem5  32439  cdj3lem2b  32469  cdj3i  32473  supssd  32723  infssd  32724  resspos  32939  resstos  32940  submarchi  33166  dfufd2  33543  tpr2rico  33858  ordtrest2NEWlem  33868  xrge0iifcnv  33879  omssubadd  34265  eulerpartlemb  34333  ballotlemfc0  34457  ballotlemfcc  34458  ftc2re  34575  loop1cycl  35105  subfacp1lem6  35153  iccllysconn  35218  cvmfolem  35247  satfsschain  35332  satfrel  35335  satfdm  35337  sat1el2xp  35347  satffunlem1lem1  35370  dmopab3rexdif  35373  satffunlem2lem2  35374  satffun  35377  fundmpss  35730  dfon2lem3  35749  dfon2lem6  35752  axextbdist  35764  dfrdg4  35915  5segofs  35970  cgrextend  35972  segconeu  35975  btwncomim  35977  btwnswapid  35981  btwnintr  35983  btwnexch3  35984  btwndiff  35991  ifscgr  36008  cgrxfr  36019  btwnxfr  36020  lineext  36040  brofs2  36041  linecgr  36045  lineid  36047  idinside  36048  endofsegid  36049  btwnconn1lem13  36063  btwnconn3  36067  finminlem  36284  nn0prpwlem  36288  cldbnd  36292  clsint2  36295  fnessref  36323  neibastop3  36328  fgmin  36336  onsuct0  36407  limsucncmpi  36411  bj-nnfea  36700  bj-axc14  36822  bj-restn0  37056  bj-0int  37067  wl-19.2reqv  37478  wl-aetr  37483  wl-axc11r  37484  fin2so  37567  tan2h  37572  lindsenlbs  37575  poimirlem2  37582  poimirlem9  37589  poimirlem17  37597  poimirlem18  37598  poimirlem21  37601  poimirlem23  37603  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimir  37613  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  itg2addnclem  37631  itg2addnclem2  37632  itg2gt0cn  37635  ftc1anclem5  37657  ftc1anclem6  37658  filbcmb  37700  nninfnub  37711  mettrifi  37717  geomcau  37719  istotbnd3  37731  sstotbnd2  37734  ismtybndlem  37766  heibor1lem  37769  heiborlem1  37771  heiborlem8  37778  heiborlem10  37780  heibor  37781  opidonOLD  37812  riscer  37948  crngohomfo  37966  keridl  37992  ispridl2  37998  ispridlc  38030  ac6s6  38132  eqvreltr  38563  dral1-o  38860  ax12indalem  38901  ax12inda2ALT  38902  lsatcveq0  38988  eqlkr3  39057  atlatmstc  39275  atlrelat1  39277  hlrelat2  39360  intnatN  39364  cvrexchlem  39376  cvratlem  39378  cvrat2  39386  atltcvr  39392  cvrat3  39399  cvrat4  39400  ps-1  39434  ps-2  39435  lplnnle2at  39498  lvolnle3at  39539  2llnma3r  39745  cdlemblem  39750  pmapjoin  39809  elpcliN  39850  lhpmcvr4N  39983  4atexlemnclw  40027  trlnidatb  40134  cdlemc4  40151  cdlemd3  40157  cdleme3g  40191  cdleme7d  40203  cdleme11c  40218  cdleme11dN  40219  cdleme21b  40283  cdleme21c  40284  cdleme21i  40292  cdleme22b  40298  cdleme35fnpq  40406  cdlemf1  40518  trlord  40526  cdlemg6c  40577  dihglblem6  41297  dochlkr  41342  dochkrshp  41343  dihjat1lem  41385  dochexmidlem5  41421  dochexmidlem8  41424  metakunt29  42190  qsalrel  42235  remulcand  42414  prjspner1  42581  fphpdo  42773  pellexlem5  42789  pellexlem6  42790  jm2.26lem3  42958  unxpwdom3  43052  omlimcl2  43203  oe0suclim  43239  cantnfresb  43286  tfsconcatb0  43306  naddgeoa  43356  iscard5  43498  sqrtcval  43603  ov2ssiunov2  43662  frege124d  43723  ordpss  44420  19.41rg  44521  stoweidlem34  45955  cfsetsnfsetf1  46974  fcoresf1  46984  euoreqb  47024  2reu8i  47028  ralralimp  47193  f1oresf1o2  47206  zm1nn  47217  elfz2z  47230  iccpartlt  47298  iccelpart  47307  icceuelpartlem  47309  fargshiftf1  47315  sprsymrelf1lem  47365  paireqne  47385  reuopreuprim  47400  goldbachthlem2  47420  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnofac2lem  47442  prmdvdsfmtnof1  47461  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem4  47484  fppr2odd  47605  gbegt5  47635  gbowge7  47637  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgoldbach  47691  isuspgrim0  47756  isuspgrimlem  47758  grimuhgr  47762  grimcnv  47763  grimco  47764  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  grtriprop  47792  uspgrlimlem3  47814  grlimgrtrilem2  47819  grlimgrtri  47820  grlicsym  47830  lcosslsp  48167  lindslinindsimp1  48186  snlindsntor  48200  m1modmmod  48255  itcovalt2  48411  eenglngeehlnmlem2  48472  itsclc0yqsol  48498  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  opnneilv  48588  i0oii  48599  io1ii  48600  iscnrm3lem4  48616  iscnrm3r  48628  setrec1lem4  48782  aacllem  48895