Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 28284 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  159  pm2.61d  182  sylibd  242  sylbid  243  sylibrd  262  sylbird  263  syland  605  animpimp2impd  843  ax12v2  2177  alrimdd  2212  axc16g  2258  axc16nf  2261  axc11r  2375  sb1OLD  2496  sb4a  2498  2eu1  2671  2eu1v  2672  ss2ralv  3960  ss2rexv  3961  trel3  5146  poss  5445  sess2  5493  wefrc  5518  wereu2  5521  funun  6381  ssimaex  6737  f1cofveqaeq  7008  f1imass  7014  soisoi  7075  isores3  7082  isofrlem  7087  isoselem  7088  weniso  7101  abnexg  7477  oninton  7514  orduniorsuc  7544  limuni3  7566  tfindsg  7574  limom  7594  f1o2ndf1  7823  soxp  7828  extmptsuppeq  7862  smoel  8007  tfrlem9  8031  tz7.49  8091  seqomlem1  8096  odi  8215  omass  8216  omeulem2  8219  oeordsuc  8230  oeeulem  8237  ertr  8314  swoord2  8331  ecopovtrn  8410  domtriord  8685  pssnn  8738  onomeneq  8747  unxpdomlem2  8761  isinf  8769  pssnnOLD  8774  findcard3  8794  frfi  8796  unblem3  8805  en3lplem1  9108  inf3lem5  9128  cantnfle  9167  cantnfp1lem3  9176  rankxpsuc  9344  tcrank  9346  ficardom  9423  carduni  9443  infxpenlem  9473  dfac8alem  9489  ac10ct  9494  ween  9495  alephdom  9541  alephle  9548  iscard3  9553  alephfp  9568  pwsdompw  9664  infdif  9669  cfslbn  9727  cofsmo  9729  cfcof  9734  fin1a2s  9874  domtriomlem  9902  ac6num  9939  zorn2lem3  9958  axdclem2  9980  imadomg  9994  iundom2g  10000  ficard  10025  fpwwe2lem7  10097  fpwwe2  10103  gchpwdom  10130  gchaclem  10138  tskr1om2  10228  inar1  10235  tskord  10240  tskuni  10243  grudomon  10277  grur1a  10279  grur1  10280  addnidpi  10361  ltexnq  10435  genpnnp  10465  addclprlem2  10477  mulclprlem  10479  psslinpr  10491  ltexprlem6  10501  ltexprlem7  10502  addcanpr  10506  mulgt0sr  10565  map2psrpr  10570  supsrlem  10571  axrrecex  10623  letr  10772  dedekind  10841  recex  11310  lemul12b  11535  mulgt1  11537  fimaxre2  11623  lbreu  11627  nnrecgt0  11717  nnunb  11930  bndndx  11933  zeo  12107  uzind  12113  fzind  12119  fnn0ind  12120  suprfinzcl  12136  suprzcl2  12378  zmax  12385  rpnnen1lem5  12421  xrletr  12592  qbtwnre  12633  qsqueeze  12635  qextltlem  12636  xralrple  12639  xlesubadd  12697  supxrunb1  12753  icoshft  12905  zltaddlt1le  12937  fzen  12973  elfz0fzfz0  13061  elfzmlbp  13067  elfzo0z  13128  fzofzim  13133  fzo1fzo0n0  13137  elfzodifsumelfzo  13152  ssfzoulel  13180  modadd1  13325  modmul1  13341  uzrdgfni  13375  fsuppmapnn0fiub0  13410  fsuppmapnn0ub  13412  fsuppmapnn0fz  13413  seqf1olem1  13459  seqf1olem2  13460  expnbnd  13643  faclbnd4lem4  13706  hashgt23el  13835  seqcoll  13874  hashle2pr  13887  elss2prb  13897  ccatalpha  13994  swrdsbslen  14073  swrdspsleq  14074  swrdswrdlem  14113  swrdswrd  14114  pfxccatin12lem2a  14136  pfxccatin12lem1  14137  pfxccatin12lem3  14141  swrdccat3blem  14148  reuccatpfxs1lem  14155  repswswrd  14193  cshf1  14219  swrd2lsw  14361  sqeqd  14573  sqrmo  14659  cau3lem  14762  icodiamlt  14843  limsupbnd2  14888  lo1bdd2  14929  climuni  14957  rlimcn2  14995  mulcn2  15000  o1of2  15017  rlimo1  15021  lo1le  15056  iseralt  15089  cvgrat  15287  fprodss  15350  rpnnen2lem12  15626  ruclem3  15634  sqrt2irr  15650  p1modz1  15662  dvdsmodexp  15663  dvds2lem  15670  dvdslelem  15710  dvdsabseq  15714  divalglem8  15801  bitsinv1lem  15840  sadcaddlem  15856  smu01lem  15884  smueqlem  15889  bezoutlem4  15941  dfgcd2  15945  algcvga  15975  lcmfunsnlem1  16033  lcmfunsnlem2lem1  16034  lcmfunsnlem2lem2  16035  lcmfdvdsb  16039  coprmgcdb  16045  coprmdvds2  16050  coprmprod  16057  isprm3  16079  prmdvdsfz  16101  isprm5  16103  coprm  16107  rpexp12i  16120  phibndlem  16162  dfphi2  16166  eulerthlem2  16174  odzdvds  16187  iserodd  16227  pclem  16230  pcpremul  16235  pcqcl  16248  pcdvdsb  16260  pcprmpw2  16273  difsqpwdvds  16278  pcaddlem  16279  pcmptcl  16282  pcfac  16290  prmpwdvds  16295  unbenlem  16299  prmreclem1  16307  4sqlem17  16352  vdwmc2  16370  vdwlem9  16380  vdwlem10  16381  vdwlem13  16384  vdwnnlem3  16388  ramcl  16420  prmgaplem7  16448  mreiincl  16925  initoid  17327  termoid  17328  initoeu2lem1  17340  pospo  17649  dirge  17913  cyccom  18413  gsmsymgrfixlem1  18622  oddvdsnn0  18739  oddvds  18742  odcl2  18759  gexdvds  18776  sylow2alem2  18810  sylow2a  18811  efgi2  18918  efgsrel  18927  efgs1b  18929  cyggex2  19085  telgsums  19181  pgpfac1lem2  19265  pgpfac1lem3a  19266  pgpfac1lem3  19267  pgpfac1lem5  19269  lmodfopnelem2  19739  lssssr  19793  gzrngunitlem  20231  znunit  20331  frgpcyg  20341  lsmcss  20457  obselocv  20493  obslbs  20495  mhpvarcl  20891  cply1mul  21018  gsummoncoe1  21028  cpmatacl  21416  cpmatinvcl  21417  cpmatmcllem  21418  m2cpminvid2lem  21454  mp2pm2mplem4  21509  pm2mp  21525  chfacfisf  21554  chfacfisfcpmat  21555  chfacfscmul0  21558  chfacfpmmul0  21562  cayhamlem4  21588  ordtrest2lem  21903  leordtval2  21912  lecldbas  21919  cncls  21974  cncnp  21980  cnpresti  21988  lmcnp  22004  cnt0  22046  isreg2  22077  cmpsublem  22099  cmpsub  22100  tgcmp  22101  bwth  22110  dfconn2  22119  1stcfb  22145  1stcelcls  22161  islly2  22184  dislly  22197  reftr  22214  comppfsc  22232  kgencn2  22257  txcnp  22320  txindis  22334  txcmplem1  22341  txlm  22348  xkohaus  22353  cnmptcom  22378  kqfvima  22430  isr0  22437  fgss2  22574  fbasrn  22584  filuni  22585  ufilmax  22607  isufil2  22608  cfinufil  22628  fmfnfmlem1  22654  fmfnfmlem2  22655  fmfnfmlem4  22657  fmfnfm  22658  fmco  22661  flimopn  22675  hausflim  22681  flimrest  22683  fclsopn  22714  flimfnfcls  22728  alexsubALTlem2  22748  alexsubALTlem3  22749  alexsubALT  22751  ptcmplem2  22753  cnextcn  22767  symgtgp  22806  qustgplem  22821  tsmsres  22844  tsmsxplem1  22853  isucn2  22980  imasdsf1olem  23075  bldisj  23100  blssps  23126  blss  23127  metcnp3  23242  ngptgp  23338  nrginvrcn  23394  nmoleub  23433  xrsmopn  23513  icccmplem3  23525  reconnlem2  23528  rectbntr0  23533  rescncf  23598  iocopnst  23641  iccpnfcnv  23645  lebnumii  23667  nmoleub2lem  23815  nmhmcn  23821  iscfil3  23973  iscau2  23977  iscau3  23978  iscau4  23979  iscmet3lem2  23992  caussi  23997  equivcfil  23999  equivcau  24000  ivthlem2  24152  ivthlem3  24153  ovoliunlem2  24203  ovoliunnul  24207  ioombl1lem4  24261  dyadmax  24298  dyadmbl  24300  volsup2  24305  itg2le  24439  itg2const2  24441  itg2seq  24442  itgsplitioo  24537  rolle  24689  c1lip1  24696  dvivthlem1  24707  lhop1  24713  dvcnvrelem1  24716  dvfsumrlim  24730  ply1divmo  24835  ig1peu  24871  plypf1  24908  coeaddlem  24945  fta1  25003  quotcan  25004  aalioulem4  25030  ulmcaulem  25088  ulmcn  25093  pilem2  25146  sincosq1lem  25189  sinq12gt0  25199  sinq12ge0  25200  tanord1  25228  lognegb  25280  logrec  25448  logbgcd1irr  25479  dcubic  25531  xrlimcnp  25653  o1cxp  25659  ftalem2  25758  ftalem3  25759  fsumdvdscom  25869  chtub  25895  vmasum  25899  bcmono  25960  bposlem3  25969  bposlem7  25973  lgsdir  26015  lgsqrlem2  26030  lgsqrmodndvds  26036  gausslemma2dlem6  26055  gausslemma2d  26057  lgsquadlem2  26064  2lgslem3a1  26083  2lgslem3b1  26084  2lgslem3c1  26085  2lgslem3d1  26086  2sqlem6  26106  2sq2  26116  2sqmod  26119  dchrisumlem3  26174  pntrsumbnd2  26250  pntpbnd1  26269  pntibnd  26276  pntlem3  26292  pntleml  26294  brbtwn2  26798  colinearalg  26803  axcontlem10  26866  edgupgr  27026  edglnl  27035  usgruspgrb  27073  subupgr  27176  uhgrspan1  27192  usgredgsscusgredg  27348  fusgrn0degnn0  27388  upgrewlkle2  27495  uspgr2wlkeq  27534  redwlk  27561  wlkdlem2  27572  upgrwlkdvdelem  27624  pthdlem1  27654  pthdlem2  27656  crctcshwlkn0lem3  27697  wlkiswwlks1  27752  wwlksm1edg  27766  wwlksnred  27777  wwlksnextbi  27779  umgr2adedgspth  27833  clwlkclwwlklem2fv2  27880  clwlkclwwlklem2a  27882  clwlkclwwlkf1lem3  27890  clwwisshclwwslemlem  27897  clwwlkf  27931  clwwlkext2edg  27940  wwlksubclwwlk  27942  clwwlknonex2lem2  27992  eupth2lems  28122  frgrwopreglem4a  28194  frgrregorufrg  28210  ex-natded5.3-2  28292  isgrpo  28379  vacn  28576  ubthlem2  28753  htthlem  28799  normgt0  29009  shmodsi  29271  spansneleq  29452  h1datomi  29463  nmcexi  29908  pjnormssi  30050  stm1add3i  30129  golem2  30154  cvnsym  30172  dmdmd  30182  mdslmd1lem1  30207  mdslmd1i  30211  mdexchi  30217  atcveq0  30230  superpos  30236  hatomistici  30244  atoml2i  30265  atcvat2i  30269  chirredlem1  30272  atcvat3i  30278  mdsymlem3  30287  mdsymlem5  30289  cdj3lem2b  30319  cdj3i  30323  supssd  30568  infssd  30569  resspos  30768  resstos  30769  submarchi  30966  tpr2rico  31383  ordtrest2NEWlem  31393  xrge0iifcnv  31404  omssubadd  31786  eulerpartlemb  31854  ballotlemfc0  31978  ballotlemfcc  31979  ftc2re  32097  loop1cycl  32615  subfacp1lem6  32663  iccllysconn  32728  cvmfolem  32757  satfsschain  32842  satfrel  32845  satfdm  32847  sat1el2xp  32857  satffunlem1lem1  32880  dmopab3rexdif  32883  satffunlem2lem2  32884  satffun  32887  fundmpss  33256  dfon2lem3  33277  dfon2lem6  33280  axextbdist  33292  trpredtr  33316  trpredmintr  33317  dftrpred3g  33319  trpredrec  33324  frpomin  33325  frmin  33334  soseq  33357  sltres  33430  nosepon  33433  nolesgn2o  33439  nogesgn1o  33441  nodenselem8  33459  nosupbnd1lem1  33476  madess  33616  madebdaylemlrcut  33636  no3indslem  33662  dfrdg4  33802  5segofs  33857  cgrextend  33859  segconeu  33862  btwncomim  33864  btwnswapid  33868  btwnintr  33870  btwnexch3  33871  btwndiff  33878  ifscgr  33895  cgrxfr  33906  btwnxfr  33907  lineext  33927  brofs2  33928  linecgr  33932  lineid  33934  idinside  33935  endofsegid  33936  btwnconn1lem13  33950  btwnconn3  33954  finminlem  34056  nn0prpwlem  34060  cldbnd  34064  clsint2  34067  fnessref  34095  neibastop3  34100  fgmin  34108  onsuct0  34179  limsucncmpi  34183  bj-nnfea  34460  bj-axc14  34576  bj-restn0  34785  bj-0int  34796  wl-19.2reqv  35209  wl-aetr  35214  wl-axc11r  35215  fin2so  35324  tan2h  35329  lindsenlbs  35332  poimirlem2  35339  poimirlem9  35346  poimirlem17  35354  poimirlem18  35355  poimirlem21  35358  poimirlem23  35360  poimirlem26  35363  poimirlem29  35366  poimirlem30  35367  poimirlem31  35368  poimir  35370  heicant  35372  mblfinlem2  35375  mblfinlem3  35376  itg2addnclem  35388  itg2addnclem2  35389  itg2gt0cn  35392  ftc1anclem5  35414  ftc1anclem6  35415  filbcmb  35458  nninfnub  35469  mettrifi  35475  geomcau  35477  istotbnd3  35489  sstotbnd2  35492  ismtybndlem  35524  heibor1lem  35527  heiborlem1  35529  heiborlem8  35536  heiborlem10  35538  heibor  35539  opidonOLD  35570  riscer  35706  crngohomfo  35724  keridl  35750  ispridl2  35756  ispridlc  35788  ac6s6  35890  eqvreltr  36282  dral1-o  36480  ax12indalem  36521  ax12inda2ALT  36522  lsatcveq0  36608  eqlkr3  36677  atlatmstc  36895  atlrelat1  36897  hlrelat2  36979  intnatN  36983  cvrexchlem  36995  cvratlem  36997  cvrat2  37005  atltcvr  37011  cvrat3  37018  cvrat4  37019  ps-1  37053  ps-2  37054  lplnnle2at  37117  lvolnle3at  37158  2llnma3r  37364  cdlemblem  37369  pmapjoin  37428  elpcliN  37469  lhpmcvr4N  37602  4atexlemnclw  37646  trlnidatb  37753  cdlemc4  37770  cdlemd3  37776  cdleme3g  37810  cdleme7d  37822  cdleme11c  37837  cdleme11dN  37838  cdleme21b  37902  cdleme21c  37903  cdleme21i  37911  cdleme22b  37917  cdleme35fnpq  38025  cdlemf1  38137  trlord  38145  cdlemg6c  38196  dihglblem6  38916  dochlkr  38961  dochkrshp  38962  dihjat1lem  39004  dochexmidlem5  39040  dochexmidlem8  39043  metakunt29  39675  qsalrel  39721  remulcand  39917  prjspner1  39960  fphpdo  40131  pellexlem5  40147  pellexlem6  40148  jm2.26lem3  40315  unxpwdom3  40412  iscard5  40615  sqrtcval  40714  ov2ssiunov2  40774  frege124d  40835  ordpss  41528  19.41rg  41629  stoweidlem34  43042  euoreqb  44033  2reu8i  44037  ralralimp  44202  f1oresf1o2  44215  zm1nn  44227  elfz2z  44240  iccpartlt  44309  iccelpart  44318  icceuelpartlem  44320  fargshiftf1  44326  sprsymrelf1lem  44376  paireqne  44396  reuopreuprim  44411  goldbachthlem2  44431  odz2prm2pw  44448  fmtnoprmfac1lem  44449  fmtnofac2lem  44453  prmdvdsfmtnof1  44472  sfprmdvdsmersenne  44488  lighneallem2  44491  lighneallem4  44495  fppr2odd  44616  gbegt5  44646  gbowge7  44648  bgoldbtbndlem4  44693  bgoldbtbnd  44694  tgoldbach  44702  isomuspgrlem2b  44714  isomgrsym  44721  zrtermorngc  44992  zrtermoringc  45061  lcosslsp  45212  lindslinindsimp1  45231  snlindsntor  45245  m1modmmod  45300  itcovalt2  45456  eenglngeehlnmlem2  45517  itsclc0yqsol  45543  itschlc0xyqsol1  45545  itschlc0xyqsol  45546  opnneilv  45584  setrec1lem4  45611  aacllem  45720