Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 29633 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  604  animpimp2impd  845  ax12v2  2174  alrimdd  2208  axc16g  2252  axc16nf  2255  axc11r  2366  sb4a  2480  2eu1  2647  2eu1v  2648  ss2ralv  4051  ss2rexv  4052  trel3  5274  poss  5589  sess2  5644  wefrc  5669  wereu2  5672  predtrss  6320  frpomin  6338  funun  6591  ssimaex  6972  f1cofveqaeq  7252  f1imass  7258  soisoi  7320  isores3  7327  isofrlem  7332  isoselem  7333  weniso  7346  abnexg  7738  oninton  7778  orduniorsuc  7813  limuni3  7836  tfindsg  7845  limom  7866  f1o2ndf1  8103  soxp  8110  xpord3inddlem  8135  soseq  8140  extmptsuppeq  8168  smoel  8355  tfrlem9  8380  tz7.49  8440  seqomlem1  8445  odi  8575  omass  8576  omeulem2  8579  oeordsuc  8590  oeeulem  8597  ertr  8714  swoord2  8731  ecopovtrn  8810  domtriord  9119  pssnn  9164  onomeneqOLD  9225  unxpdomlem2  9247  isinf  9256  isinfOLD  9257  pssnnOLD  9261  f1finf1o  9267  findcard3  9281  findcard3OLD  9282  frfi  9284  unblem3  9293  en3lplem1  9603  inf3lem5  9623  cantnfle  9662  cantnfp1lem3  9671  ttrcltr  9707  frmin  9740  rankxpsuc  9873  tcrank  9875  ficardom  9952  carduni  9972  infxpenlem  10004  dfac8alem  10020  ac10ct  10025  ween  10026  alephdom  10072  alephle  10079  iscard3  10084  alephfp  10099  pwsdompw  10195  infdif  10200  cfslbn  10258  cofsmo  10260  cfcof  10265  fin1a2s  10405  domtriomlem  10433  ac6num  10470  zorn2lem3  10489  axdclem2  10511  imadomg  10525  iundom2g  10531  ficard  10556  fpwwe2lem7  10628  fpwwe2  10634  gchpwdom  10661  gchaclem  10669  tskr1om2  10759  inar1  10766  tskord  10771  tskuni  10774  grudomon  10808  grur1a  10810  grur1  10811  addnidpi  10892  ltexnq  10966  genpnnp  10996  addclprlem2  11008  mulclprlem  11010  psslinpr  11022  ltexprlem6  11032  ltexprlem7  11033  addcanpr  11037  mulgt0sr  11096  map2psrpr  11101  supsrlem  11102  axrrecex  11154  letr  11304  dedekind  11373  recex  11842  lemul12b  12067  mulgt1  12069  fimaxre2  12155  lbreu  12160  nnrecgt0  12251  nnunb  12464  bndndx  12467  zeo  12644  uzind  12650  fzind  12656  fnn0ind  12657  suprfinzcl  12672  suprzcl2  12918  zmax  12925  rpnnen1lem5  12961  xrletr  13133  qbtwnre  13174  qsqueeze  13176  qextltlem  13177  xralrple  13180  xlesubadd  13238  supxrunb1  13294  icoshft  13446  zltaddlt1le  13478  fzen  13514  elfz0fzfz0  13602  elfzmlbp  13608  elfzo0z  13670  fzofzim  13675  fzo1fzo0n0  13679  elfzodifsumelfzo  13694  ssfzoulel  13722  modadd1  13869  modmul1  13885  uzrdgfni  13919  fsuppmapnn0fiub0  13954  fsuppmapnn0ub  13956  fsuppmapnn0fz  13957  seqf1olem1  14003  seqf1olem2  14004  expnbnd  14191  faclbnd4lem4  14252  hashgt23el  14380  seqcoll  14421  hashle2pr  14434  elss2prb  14444  ccatalpha  14539  swrdsbslen  14610  swrdspsleq  14611  swrdswrdlem  14650  swrdswrd  14651  pfxccatin12lem2a  14673  pfxccatin12lem1  14674  pfxccatin12lem3  14678  swrdccat3blem  14685  reuccatpfxs1lem  14692  repswswrd  14730  cshf1  14756  swrd2lsw  14899  sqeqd  15109  sqrmo  15194  cau3lem  15297  icodiamlt  15378  limsupbnd2  15423  lo1bdd2  15464  climuni  15492  rlimcn3  15530  mulcn2  15536  o1of2  15553  rlimo1  15557  lo1le  15594  iseralt  15627  cvgrat  15825  fprodss  15888  rpnnen2lem12  16164  ruclem3  16172  sqrt2irr  16188  p1modz1  16200  dvdsmodexp  16201  dvds2lem  16208  dvdslelem  16248  dvdsabseq  16252  divalglem8  16339  bitsinv1lem  16378  sadcaddlem  16394  smu01lem  16422  smueqlem  16427  bezoutlem4  16480  dfgcd2  16484  algcvga  16512  lcmfunsnlem1  16570  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  lcmfdvdsb  16576  coprmgcdb  16582  coprmdvds2  16587  coprmprod  16594  isprm3  16616  prmdvdsfz  16638  isprm5  16640  coprm  16644  rpexp12i  16657  phibndlem  16699  dfphi2  16703  eulerthlem2  16711  odzdvds  16724  iserodd  16764  pclem  16767  pcpremul  16772  pcqcl  16785  pcdvdsb  16798  pcprmpw2  16811  difsqpwdvds  16816  pcaddlem  16817  pcmptcl  16820  pcfac  16828  prmpwdvds  16833  unbenlem  16837  prmreclem1  16845  4sqlem17  16890  vdwmc2  16908  vdwlem9  16918  vdwlem10  16919  vdwlem13  16922  vdwnnlem3  16926  ramcl  16958  prmgaplem7  16986  mreiincl  17536  initoid  17947  termoid  17948  initoeu2lem1  17960  pospo  18294  dirge  18552  cyccom  19074  gsmsymgrfixlem1  19288  oddvdsnn0  19405  oddvds  19408  odcl2  19426  gexdvds  19445  sylow2alem2  19479  sylow2a  19480  efgi2  19586  efgsrel  19595  efgs1b  19597  imasabl  19736  cyggex2  19757  telgsums  19853  pgpfac1lem2  19937  pgpfac1lem3a  19938  pgpfac1lem3  19939  pgpfac1lem5  19941  lmodfopnelem2  20497  lssssr  20552  gzrngunitlem  20995  znunit  21103  frgpcyg  21113  lsmcss  21229  obselocv  21267  obslbs  21269  mhpvarcl  21673  cply1mul  21800  gsummoncoe1  21810  cpmatacl  22200  cpmatinvcl  22201  cpmatmcllem  22202  m2cpminvid2lem  22238  mp2pm2mplem4  22293  pm2mp  22309  chfacfisf  22338  chfacfisfcpmat  22339  chfacfscmul0  22342  chfacfpmmul0  22346  cayhamlem4  22372  ordtrest2lem  22689  leordtval2  22698  lecldbas  22705  cncls  22760  cncnp  22766  cnpresti  22774  lmcnp  22790  cnt0  22832  isreg2  22863  cmpsublem  22885  cmpsub  22886  tgcmp  22887  bwth  22896  dfconn2  22905  1stcfb  22931  1stcelcls  22947  islly2  22970  dislly  22983  reftr  23000  comppfsc  23018  kgencn2  23043  txcnp  23106  txindis  23120  txcmplem1  23127  txlm  23134  xkohaus  23139  cnmptcom  23164  kqfvima  23216  isr0  23223  fgss2  23360  fbasrn  23370  filuni  23371  ufilmax  23393  isufil2  23394  cfinufil  23414  fmfnfmlem1  23440  fmfnfmlem2  23441  fmfnfmlem4  23443  fmfnfm  23444  fmco  23447  flimopn  23461  hausflim  23467  flimrest  23469  fclsopn  23500  flimfnfcls  23514  alexsubALTlem2  23534  alexsubALTlem3  23535  alexsubALT  23537  ptcmplem2  23539  cnextcn  23553  symgtgp  23592  qustgplem  23607  tsmsres  23630  tsmsxplem1  23639  isucn2  23766  imasdsf1olem  23861  bldisj  23886  blssps  23912  blss  23913  metcnp3  24031  ngptgp  24127  nrginvrcn  24191  nmoleub  24230  xrsmopn  24310  icccmplem3  24322  reconnlem2  24325  rectbntr0  24330  rescncf  24395  iocopnst  24438  iccpnfcnv  24442  lebnumii  24464  nmoleub2lem  24612  nmhmcn  24618  iscfil3  24772  iscau2  24776  iscau3  24777  iscau4  24778  iscmet3lem2  24791  caussi  24796  equivcfil  24798  equivcau  24799  ivthlem2  24951  ivthlem3  24952  ovoliunlem2  25002  ovoliunnul  25006  ioombl1lem4  25060  dyadmax  25097  dyadmbl  25099  volsup2  25104  itg2le  25239  itg2const2  25241  itg2seq  25242  itgsplitioo  25337  rolle  25489  c1lip1  25496  dvivthlem1  25507  lhop1  25513  dvcnvrelem1  25516  dvfsumrlim  25530  ply1divmo  25635  ig1peu  25671  plypf1  25708  coeaddlem  25745  fta1  25803  quotcan  25804  aalioulem4  25830  ulmcaulem  25888  ulmcn  25893  pilem2  25946  sincosq1lem  25989  sinq12gt0  25999  sinq12ge0  26000  tanord1  26028  lognegb  26080  logrec  26248  logbgcd1irr  26279  dcubic  26331  xrlimcnp  26453  o1cxp  26459  ftalem2  26558  ftalem3  26559  fsumdvdscom  26669  chtub  26695  vmasum  26699  bcmono  26760  bposlem3  26769  bposlem7  26773  lgsdir  26815  lgsqrlem2  26830  lgsqrmodndvds  26836  gausslemma2dlem6  26855  gausslemma2d  26857  lgsquadlem2  26864  2lgslem3a1  26883  2lgslem3b1  26884  2lgslem3c1  26885  2lgslem3d1  26886  2sqlem6  26906  2sq2  26916  2sqmod  26919  dchrisumlem3  26974  pntrsumbnd2  27050  pntpbnd1  27069  pntibnd  27076  pntlem3  27092  pntleml  27094  sltres  27145  nosepon  27148  nolesgn2o  27154  nogesgn1o  27156  nodenselem8  27174  nosupbnd1lem1  27191  madess  27351  madebdaylemlrcut  27373  brbtwn2  28143  colinearalg  28148  axcontlem10  28211  edgupgr  28374  edglnl  28383  usgruspgrb  28421  subupgr  28524  uhgrspan1  28540  usgredgsscusgredg  28696  fusgrn0degnn0  28736  upgrewlkle2  28843  uspgr2wlkeq  28883  redwlk  28909  wlkdlem2  28920  upgrwlkdvdelem  28973  pthdlem1  29003  pthdlem2  29005  crctcshwlkn0lem3  29046  wlkiswwlks1  29101  wwlksm1edg  29115  wwlksnred  29126  wwlksnextbi  29128  umgr2adedgspth  29182  clwlkclwwlklem2fv2  29229  clwlkclwwlklem2a  29231  clwlkclwwlkf1lem3  29239  clwwisshclwwslemlem  29246  clwwlkf  29280  clwwlkext2edg  29289  wwlksubclwwlk  29291  clwwlknonex2lem2  29341  eupth2lems  29471  frgrwopreglem4a  29543  frgrregorufrg  29559  ex-natded5.3-2  29641  isgrpo  29728  vacn  29925  ubthlem2  30102  htthlem  30148  normgt0  30358  shmodsi  30620  spansneleq  30801  h1datomi  30812  nmcexi  31257  pjnormssi  31399  stm1add3i  31478  golem2  31503  cvnsym  31521  dmdmd  31531  mdslmd1lem1  31556  mdslmd1i  31560  mdexchi  31566  atcveq0  31579  superpos  31585  hatomistici  31593  atoml2i  31614  atcvat2i  31618  chirredlem1  31621  atcvat3i  31627  mdsymlem3  31636  mdsymlem5  31638  cdj3lem2b  31668  cdj3i  31672  supssd  31912  infssd  31913  resspos  32114  resstos  32115  submarchi  32310  tpr2rico  32830  ordtrest2NEWlem  32840  xrge0iifcnv  32851  omssubadd  33237  eulerpartlemb  33305  ballotlemfc0  33429  ballotlemfcc  33430  ftc2re  33548  loop1cycl  34066  subfacp1lem6  34114  iccllysconn  34179  cvmfolem  34208  satfsschain  34293  satfrel  34296  satfdm  34298  sat1el2xp  34308  satffunlem1lem1  34331  dmopab3rexdif  34334  satffunlem2lem2  34335  satffun  34338  fundmpss  34676  dfon2lem3  34695  dfon2lem6  34698  axextbdist  34710  dfrdg4  34861  5segofs  34916  cgrextend  34918  segconeu  34921  btwncomim  34923  btwnswapid  34927  btwnintr  34929  btwnexch3  34930  btwndiff  34937  ifscgr  34954  cgrxfr  34965  btwnxfr  34966  lineext  34986  brofs2  34987  linecgr  34991  lineid  34993  idinside  34994  endofsegid  34995  btwnconn1lem13  35009  btwnconn3  35013  finminlem  35141  nn0prpwlem  35145  cldbnd  35149  clsint2  35152  fnessref  35180  neibastop3  35185  fgmin  35193  onsuct0  35264  limsucncmpi  35268  bj-nnfea  35550  bj-axc14  35673  bj-restn0  35909  bj-0int  35920  wl-19.2reqv  36331  wl-aetr  36336  wl-axc11r  36337  fin2so  36413  tan2h  36418  lindsenlbs  36421  poimirlem2  36428  poimirlem9  36435  poimirlem17  36443  poimirlem18  36444  poimirlem21  36447  poimirlem23  36449  poimirlem26  36452  poimirlem29  36455  poimirlem30  36456  poimirlem31  36457  poimir  36459  heicant  36461  mblfinlem2  36464  mblfinlem3  36465  itg2addnclem  36477  itg2addnclem2  36478  itg2gt0cn  36481  ftc1anclem5  36503  ftc1anclem6  36504  filbcmb  36546  nninfnub  36557  mettrifi  36563  geomcau  36565  istotbnd3  36577  sstotbnd2  36580  ismtybndlem  36612  heibor1lem  36615  heiborlem1  36617  heiborlem8  36624  heiborlem10  36626  heibor  36627  opidonOLD  36658  riscer  36794  crngohomfo  36812  keridl  36838  ispridl2  36844  ispridlc  36876  ac6s6  36978  eqvreltr  37415  dral1-o  37712  ax12indalem  37753  ax12inda2ALT  37754  lsatcveq0  37840  eqlkr3  37909  atlatmstc  38127  atlrelat1  38129  hlrelat2  38212  intnatN  38216  cvrexchlem  38228  cvratlem  38230  cvrat2  38238  atltcvr  38244  cvrat3  38251  cvrat4  38252  ps-1  38286  ps-2  38287  lplnnle2at  38350  lvolnle3at  38391  2llnma3r  38597  cdlemblem  38602  pmapjoin  38661  elpcliN  38702  lhpmcvr4N  38835  4atexlemnclw  38879  trlnidatb  38986  cdlemc4  39003  cdlemd3  39009  cdleme3g  39043  cdleme7d  39055  cdleme11c  39070  cdleme11dN  39071  cdleme21b  39135  cdleme21c  39136  cdleme21i  39144  cdleme22b  39150  cdleme35fnpq  39258  cdlemf1  39370  trlord  39378  cdlemg6c  39429  dihglblem6  40149  dochlkr  40194  dochkrshp  40195  dihjat1lem  40237  dochexmidlem5  40273  dochexmidlem8  40276  metakunt29  40951  qsalrel  41011  remulcand  41255  prjspner1  41312  fphpdo  41488  pellexlem5  41504  pellexlem6  41505  jm2.26lem3  41673  unxpwdom3  41770  omlimcl2  41924  oe0suclim  41960  cantnfresb  42007  tfsconcatb0  42027  naddsuc2  42076  naddgeoa  42078  iscard5  42220  sqrtcval  42325  ov2ssiunov2  42384  frege124d  42445  ordpss  43143  19.41rg  43244  stoweidlem34  44685  cfsetsnfsetf1  45704  fcoresf1  45714  euoreqb  45752  2reu8i  45756  ralralimp  45921  f1oresf1o2  45934  zm1nn  45945  elfz2z  45958  iccpartlt  46027  iccelpart  46036  icceuelpartlem  46038  fargshiftf1  46044  sprsymrelf1lem  46094  paireqne  46114  reuopreuprim  46129  goldbachthlem2  46149  odz2prm2pw  46166  fmtnoprmfac1lem  46167  fmtnofac2lem  46171  prmdvdsfmtnof1  46190  sfprmdvdsmersenne  46206  lighneallem2  46209  lighneallem4  46213  fppr2odd  46334  gbegt5  46364  gbowge7  46366  bgoldbtbndlem4  46411  bgoldbtbnd  46412  tgoldbach  46420  isomuspgrlem2b  46432  isomgrsym  46439  rnglidlmcl  46681  zrtermorngc  46801  zrtermoringc  46870  lcosslsp  47021  lindslinindsimp1  47040  snlindsntor  47054  m1modmmod  47109  itcovalt2  47265  eenglngeehlnmlem2  47326  itsclc0yqsol  47352  itschlc0xyqsol1  47354  itschlc0xyqsol  47355  opnneilv  47443  i0oii  47454  io1ii  47455  iscnrm3lem4  47471  iscnrm3r  47483  setrec1lem4  47637  aacllem  47750