Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 28665 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  258  sylbird  259  syland  602  animpimp2impd  842  ax12v2  2175  alrimdd  2210  axc16g  2255  axc16nf  2258  axc11r  2366  sb1OLD  2482  sb4a  2484  2eu1  2652  2eu1v  2653  ss2ralv  3985  ss2rexv  3986  trel3  5195  poss  5496  sess2  5549  wefrc  5574  wereu2  5577  predtrss  6214  frpomin  6228  funun  6464  ssimaex  6835  f1cofveqaeq  7112  f1imass  7118  soisoi  7179  isores3  7186  isofrlem  7191  isoselem  7192  weniso  7205  abnexg  7584  oninton  7622  orduniorsuc  7652  limuni3  7674  tfindsg  7682  limom  7703  f1o2ndf1  7934  soxp  7941  extmptsuppeq  7975  smoel  8162  tfrlem9  8187  tz7.49  8246  seqomlem1  8251  odi  8372  omass  8373  omeulem2  8376  oeordsuc  8387  oeeulem  8394  ertr  8471  swoord2  8488  ecopovtrn  8567  domtriord  8859  pssnn  8913  onomeneq  8943  unxpdomlem2  8957  isinf  8965  pssnnOLD  8969  findcard3  8987  frfi  8989  unblem3  8998  en3lplem1  9300  inf3lem5  9320  cantnfle  9359  cantnfp1lem3  9368  trpredtr  9408  trpredmintr  9409  dftrpred3g  9412  trpredrec  9415  frmin  9438  rankxpsuc  9571  tcrank  9573  ficardom  9650  carduni  9670  infxpenlem  9700  dfac8alem  9716  ac10ct  9721  ween  9722  alephdom  9768  alephle  9775  iscard3  9780  alephfp  9795  pwsdompw  9891  infdif  9896  cfslbn  9954  cofsmo  9956  cfcof  9961  fin1a2s  10101  domtriomlem  10129  ac6num  10166  zorn2lem3  10185  axdclem2  10207  imadomg  10221  iundom2g  10227  ficard  10252  fpwwe2lem7  10324  fpwwe2  10330  gchpwdom  10357  gchaclem  10365  tskr1om2  10455  inar1  10462  tskord  10467  tskuni  10470  grudomon  10504  grur1a  10506  grur1  10507  addnidpi  10588  ltexnq  10662  genpnnp  10692  addclprlem2  10704  mulclprlem  10706  psslinpr  10718  ltexprlem6  10728  ltexprlem7  10729  addcanpr  10733  mulgt0sr  10792  map2psrpr  10797  supsrlem  10798  axrrecex  10850  letr  10999  dedekind  11068  recex  11537  lemul12b  11762  mulgt1  11764  fimaxre2  11850  lbreu  11855  nnrecgt0  11946  nnunb  12159  bndndx  12162  zeo  12336  uzind  12342  fzind  12348  fnn0ind  12349  suprfinzcl  12365  suprzcl2  12607  zmax  12614  rpnnen1lem5  12650  xrletr  12821  qbtwnre  12862  qsqueeze  12864  qextltlem  12865  xralrple  12868  xlesubadd  12926  supxrunb1  12982  icoshft  13134  zltaddlt1le  13166  fzen  13202  elfz0fzfz0  13290  elfzmlbp  13296  elfzo0z  13357  fzofzim  13362  fzo1fzo0n0  13366  elfzodifsumelfzo  13381  ssfzoulel  13409  modadd1  13556  modmul1  13572  uzrdgfni  13606  fsuppmapnn0fiub0  13641  fsuppmapnn0ub  13643  fsuppmapnn0fz  13644  seqf1olem1  13690  seqf1olem2  13691  expnbnd  13875  faclbnd4lem4  13938  hashgt23el  14067  seqcoll  14106  hashle2pr  14119  elss2prb  14129  ccatalpha  14226  swrdsbslen  14305  swrdspsleq  14306  swrdswrdlem  14345  swrdswrd  14346  pfxccatin12lem2a  14368  pfxccatin12lem1  14369  pfxccatin12lem3  14373  swrdccat3blem  14380  reuccatpfxs1lem  14387  repswswrd  14425  cshf1  14451  swrd2lsw  14593  sqeqd  14805  sqrmo  14891  cau3lem  14994  icodiamlt  15075  limsupbnd2  15120  lo1bdd2  15161  climuni  15189  rlimcn3  15227  mulcn2  15233  o1of2  15250  rlimo1  15254  lo1le  15291  iseralt  15324  cvgrat  15523  fprodss  15586  rpnnen2lem12  15862  ruclem3  15870  sqrt2irr  15886  p1modz1  15898  dvdsmodexp  15899  dvds2lem  15906  dvdslelem  15946  dvdsabseq  15950  divalglem8  16037  bitsinv1lem  16076  sadcaddlem  16092  smu01lem  16120  smueqlem  16125  bezoutlem4  16178  dfgcd2  16182  algcvga  16212  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfdvdsb  16276  coprmgcdb  16282  coprmdvds2  16287  coprmprod  16294  isprm3  16316  prmdvdsfz  16338  isprm5  16340  coprm  16344  rpexp12i  16357  phibndlem  16399  dfphi2  16403  eulerthlem2  16411  odzdvds  16424  iserodd  16464  pclem  16467  pcpremul  16472  pcqcl  16485  pcdvdsb  16498  pcprmpw2  16511  difsqpwdvds  16516  pcaddlem  16517  pcmptcl  16520  pcfac  16528  prmpwdvds  16533  unbenlem  16537  prmreclem1  16545  4sqlem17  16590  vdwmc2  16608  vdwlem9  16618  vdwlem10  16619  vdwlem13  16622  vdwnnlem3  16626  ramcl  16658  prmgaplem7  16686  mreiincl  17222  initoid  17632  termoid  17633  initoeu2lem1  17645  pospo  17978  dirge  18236  cyccom  18737  gsmsymgrfixlem1  18950  oddvdsnn0  19067  oddvds  19070  odcl2  19087  gexdvds  19104  sylow2alem2  19138  sylow2a  19139  efgi2  19246  efgsrel  19255  efgs1b  19257  cyggex2  19413  telgsums  19509  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem5  19597  lmodfopnelem2  20075  lssssr  20130  gzrngunitlem  20575  znunit  20683  frgpcyg  20693  lsmcss  20809  obselocv  20845  obslbs  20847  mhpvarcl  21248  cply1mul  21375  gsummoncoe1  21385  cpmatacl  21773  cpmatinvcl  21774  cpmatmcllem  21775  m2cpminvid2lem  21811  mp2pm2mplem4  21866  pm2mp  21882  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmul0  21915  chfacfpmmul0  21919  cayhamlem4  21945  ordtrest2lem  22262  leordtval2  22271  lecldbas  22278  cncls  22333  cncnp  22339  cnpresti  22347  lmcnp  22363  cnt0  22405  isreg2  22436  cmpsublem  22458  cmpsub  22459  tgcmp  22460  bwth  22469  dfconn2  22478  1stcfb  22504  1stcelcls  22520  islly2  22543  dislly  22556  reftr  22573  comppfsc  22591  kgencn2  22616  txcnp  22679  txindis  22693  txcmplem1  22700  txlm  22707  xkohaus  22712  cnmptcom  22737  kqfvima  22789  isr0  22796  fgss2  22933  fbasrn  22943  filuni  22944  ufilmax  22966  isufil2  22967  cfinufil  22987  fmfnfmlem1  23013  fmfnfmlem2  23014  fmfnfmlem4  23016  fmfnfm  23017  fmco  23020  flimopn  23034  hausflim  23040  flimrest  23042  fclsopn  23073  flimfnfcls  23087  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALT  23110  ptcmplem2  23112  cnextcn  23126  symgtgp  23165  qustgplem  23180  tsmsres  23203  tsmsxplem1  23212  isucn2  23339  imasdsf1olem  23434  bldisj  23459  blssps  23485  blss  23486  metcnp3  23602  ngptgp  23698  nrginvrcn  23762  nmoleub  23801  xrsmopn  23881  icccmplem3  23893  reconnlem2  23896  rectbntr0  23901  rescncf  23966  iocopnst  24009  iccpnfcnv  24013  lebnumii  24035  nmoleub2lem  24183  nmhmcn  24189  iscfil3  24342  iscau2  24346  iscau3  24347  iscau4  24348  iscmet3lem2  24361  caussi  24366  equivcfil  24368  equivcau  24369  ivthlem2  24521  ivthlem3  24522  ovoliunlem2  24572  ovoliunnul  24576  ioombl1lem4  24630  dyadmax  24667  dyadmbl  24669  volsup2  24674  itg2le  24809  itg2const2  24811  itg2seq  24812  itgsplitioo  24907  rolle  25059  c1lip1  25066  dvivthlem1  25077  lhop1  25083  dvcnvrelem1  25086  dvfsumrlim  25100  ply1divmo  25205  ig1peu  25241  plypf1  25278  coeaddlem  25315  fta1  25373  quotcan  25374  aalioulem4  25400  ulmcaulem  25458  ulmcn  25463  pilem2  25516  sincosq1lem  25559  sinq12gt0  25569  sinq12ge0  25570  tanord1  25598  lognegb  25650  logrec  25818  logbgcd1irr  25849  dcubic  25901  xrlimcnp  26023  o1cxp  26029  ftalem2  26128  ftalem3  26129  fsumdvdscom  26239  chtub  26265  vmasum  26269  bcmono  26330  bposlem3  26339  bposlem7  26343  lgsdir  26385  lgsqrlem2  26400  lgsqrmodndvds  26406  gausslemma2dlem6  26425  gausslemma2d  26427  lgsquadlem2  26434  2lgslem3a1  26453  2lgslem3b1  26454  2lgslem3c1  26455  2lgslem3d1  26456  2sqlem6  26476  2sq2  26486  2sqmod  26489  dchrisumlem3  26544  pntrsumbnd2  26620  pntpbnd1  26639  pntibnd  26646  pntlem3  26662  pntleml  26664  brbtwn2  27176  colinearalg  27181  axcontlem10  27244  edgupgr  27407  edglnl  27416  usgruspgrb  27454  subupgr  27557  uhgrspan1  27573  usgredgsscusgredg  27729  fusgrn0degnn0  27769  upgrewlkle2  27876  uspgr2wlkeq  27915  redwlk  27942  wlkdlem2  27953  upgrwlkdvdelem  28005  pthdlem1  28035  pthdlem2  28037  crctcshwlkn0lem3  28078  wlkiswwlks1  28133  wwlksm1edg  28147  wwlksnred  28158  wwlksnextbi  28160  umgr2adedgspth  28214  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a  28263  clwlkclwwlkf1lem3  28271  clwwisshclwwslemlem  28278  clwwlkf  28312  clwwlkext2edg  28321  wwlksubclwwlk  28323  clwwlknonex2lem2  28373  eupth2lems  28503  frgrwopreglem4a  28575  frgrregorufrg  28591  ex-natded5.3-2  28673  isgrpo  28760  vacn  28957  ubthlem2  29134  htthlem  29180  normgt0  29390  shmodsi  29652  spansneleq  29833  h1datomi  29844  nmcexi  30289  pjnormssi  30431  stm1add3i  30510  golem2  30535  cvnsym  30553  dmdmd  30563  mdslmd1lem1  30588  mdslmd1i  30592  mdexchi  30598  atcveq0  30611  superpos  30617  hatomistici  30625  atoml2i  30646  atcvat2i  30650  chirredlem1  30653  atcvat3i  30659  mdsymlem3  30668  mdsymlem5  30670  cdj3lem2b  30700  cdj3i  30704  supssd  30946  infssd  30947  resspos  31146  resstos  31147  submarchi  31342  tpr2rico  31764  ordtrest2NEWlem  31774  xrge0iifcnv  31785  omssubadd  32167  eulerpartlemb  32235  ballotlemfc0  32359  ballotlemfcc  32360  ftc2re  32478  loop1cycl  32999  subfacp1lem6  33047  iccllysconn  33112  cvmfolem  33141  satfsschain  33226  satfrel  33229  satfdm  33231  sat1el2xp  33241  satffunlem1lem1  33264  dmopab3rexdif  33267  satffunlem2lem2  33268  satffun  33271  fundmpss  33646  dfon2lem3  33667  dfon2lem6  33670  axextbdist  33682  ttrcltr  33702  soseq  33730  sltres  33792  nosepon  33795  nolesgn2o  33801  nogesgn1o  33803  nodenselem8  33821  nosupbnd1lem1  33838  madess  33986  madebdaylemlrcut  34006  dfrdg4  34180  5segofs  34235  cgrextend  34237  segconeu  34240  btwncomim  34242  btwnswapid  34246  btwnintr  34248  btwnexch3  34249  btwndiff  34256  ifscgr  34273  cgrxfr  34284  btwnxfr  34285  lineext  34305  brofs2  34306  linecgr  34310  lineid  34312  idinside  34313  endofsegid  34314  btwnconn1lem13  34328  btwnconn3  34332  finminlem  34434  nn0prpwlem  34438  cldbnd  34442  clsint2  34445  fnessref  34473  neibastop3  34478  fgmin  34486  onsuct0  34557  limsucncmpi  34561  bj-nnfea  34843  bj-axc14  34967  bj-restn0  35188  bj-0int  35199  wl-19.2reqv  35610  wl-aetr  35615  wl-axc11r  35616  fin2so  35691  tan2h  35696  lindsenlbs  35699  poimirlem2  35706  poimirlem9  35713  poimirlem17  35721  poimirlem18  35722  poimirlem21  35725  poimirlem23  35727  poimirlem26  35730  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimir  35737  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  itg2addnclem  35755  itg2addnclem2  35756  itg2gt0cn  35759  ftc1anclem5  35781  ftc1anclem6  35782  filbcmb  35825  nninfnub  35836  mettrifi  35842  geomcau  35844  istotbnd3  35856  sstotbnd2  35859  ismtybndlem  35891  heibor1lem  35894  heiborlem1  35896  heiborlem8  35903  heiborlem10  35905  heibor  35906  opidonOLD  35937  riscer  36073  crngohomfo  36091  keridl  36117  ispridl2  36123  ispridlc  36155  ac6s6  36257  eqvreltr  36647  dral1-o  36845  ax12indalem  36886  ax12inda2ALT  36887  lsatcveq0  36973  eqlkr3  37042  atlatmstc  37260  atlrelat1  37262  hlrelat2  37344  intnatN  37348  cvrexchlem  37360  cvratlem  37362  cvrat2  37370  atltcvr  37376  cvrat3  37383  cvrat4  37384  ps-1  37418  ps-2  37419  lplnnle2at  37482  lvolnle3at  37523  2llnma3r  37729  cdlemblem  37734  pmapjoin  37793  elpcliN  37834  lhpmcvr4N  37967  4atexlemnclw  38011  trlnidatb  38118  cdlemc4  38135  cdlemd3  38141  cdleme3g  38175  cdleme7d  38187  cdleme11c  38202  cdleme11dN  38203  cdleme21b  38267  cdleme21c  38268  cdleme21i  38276  cdleme22b  38282  cdleme35fnpq  38390  cdlemf1  38502  trlord  38510  cdlemg6c  38561  dihglblem6  39281  dochlkr  39326  dochkrshp  39327  dihjat1lem  39369  dochexmidlem5  39405  dochexmidlem8  39408  metakunt29  40081  qsalrel  40141  remulcand  40341  prjspner1  40384  fphpdo  40555  pellexlem5  40571  pellexlem6  40572  jm2.26lem3  40739  unxpwdom3  40836  iscard5  41039  sqrtcval  41138  ov2ssiunov2  41197  frege124d  41258  ordpss  41958  19.41rg  42059  stoweidlem34  43465  cfsetsnfsetf1  44440  fcoresf1  44450  euoreqb  44488  2reu8i  44492  ralralimp  44657  f1oresf1o2  44670  zm1nn  44682  elfz2z  44695  iccpartlt  44764  iccelpart  44773  icceuelpartlem  44775  fargshiftf1  44781  sprsymrelf1lem  44831  paireqne  44851  reuopreuprim  44866  goldbachthlem2  44886  odz2prm2pw  44903  fmtnoprmfac1lem  44904  fmtnofac2lem  44908  prmdvdsfmtnof1  44927  sfprmdvdsmersenne  44943  lighneallem2  44946  lighneallem4  44950  fppr2odd  45071  gbegt5  45101  gbowge7  45103  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgoldbach  45157  isomuspgrlem2b  45169  isomgrsym  45176  zrtermorngc  45447  zrtermoringc  45516  lcosslsp  45667  lindslinindsimp1  45686  snlindsntor  45700  m1modmmod  45755  itcovalt2  45911  eenglngeehlnmlem2  45972  itsclc0yqsol  45998  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  opnneilv  46090  i0oii  46101  io1ii  46102  iscnrm3lem4  46118  iscnrm3r  46130  setrec1lem4  46282  aacllem  46391