Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30475 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  2186  alrimdd  2221  axc16g  2267  axc16nf  2270  axc11r  2372  sb4a  2484  2eu1  2651  2eu1v  2652  ss2ralv  4004  ss2rexv  4005  trel3  5214  poss  5534  sess2  5590  wefrc  5618  wereu2  5621  predtrss  6280  frpomin  6298  funun  6538  ssimaex  6919  f1cofveqaeq  7203  f1imass  7210  soisoi  7274  isores3  7281  isofrlem  7286  isoselem  7287  weniso  7300  abnexg  7701  oninton  7740  orduniorsuc  7772  limuni3  7794  tfindsg  7803  limom  7824  resf1extb  7876  f1o2ndf1  8064  soxp  8071  xpord3inddlem  8096  soseq  8101  extmptsuppeq  8130  smoel  8292  tfrlem9  8316  tz7.49  8376  seqomlem1  8381  odi  8506  omass  8507  omeulem2  8510  oeordsuc  8522  oeeulem  8529  naddsuc2  8629  ertr  8650  swoord2  8668  ecopovtrn  8757  domtriord  9051  pssnn  9093  unxpdomlem2  9157  isinf  9165  f1finf1o  9173  findcard3  9183  frfi  9185  unblem3  9194  supssd  9366  infssd  9397  en3lplem1  9521  inf3lem5  9541  cantnfle  9580  cantnfp1lem3  9589  ttrcltr  9625  frmin  9661  rankxpsuc  9794  tcrank  9796  ficardom  9873  carduni  9893  infxpenlem  9923  dfac8alem  9939  ac10ct  9944  ween  9945  alephdom  9991  alephle  9998  iscard3  10003  alephfp  10018  pwsdompw  10113  infdif  10118  cfslbn  10177  cofsmo  10179  cfcof  10184  fin1a2s  10324  domtriomlem  10352  ac6num  10389  zorn2lem3  10408  axdclem2  10430  imadomg  10444  iundom2g  10450  ficard  10475  fpwwe2lem7  10548  fpwwe2  10554  gchpwdom  10581  gchaclem  10589  tskr1om2  10679  inar1  10686  tskord  10691  tskuni  10694  grudomon  10728  grur1a  10730  grur1  10731  addnidpi  10812  ltexnq  10886  genpnnp  10916  addclprlem2  10928  mulclprlem  10930  psslinpr  10942  ltexprlem6  10952  ltexprlem7  10953  addcanpr  10957  mulgt0sr  11016  map2psrpr  11021  supsrlem  11022  axrrecex  11074  letr  11227  dedekind  11296  recex  11769  lemul12b  11998  mulgt1OLD  12000  fimaxre2  12087  lbreu  12092  nnrecgt0  12188  nnunb  12397  bndndx  12400  zeo  12578  uzind  12584  fzind  12590  fnn0ind  12591  suprfinzcl  12606  suprzcl2  12851  zmax  12858  rpnnen1lem5  12894  xrletr  13072  qbtwnre  13114  qsqueeze  13116  qextltlem  13117  xralrple  13120  xlesubadd  13178  supxrunb1  13234  icoshft  13389  zltaddlt1le  13421  fzen  13457  elfz0fzfz0  13549  elfzmlbp  13555  elfzo0z  13617  fzofzim  13625  fzo1fzo0n0  13631  elfzodifsumelfzo  13647  ssfzoulel  13676  modadd1  13828  modmul1  13847  uzrdgfni  13881  fsuppmapnn0fiub0  13916  fsuppmapnn0ub  13918  fsuppmapnn0fz  13919  seqf1olem1  13964  seqf1olem2  13965  expnbnd  14155  faclbnd4lem4  14219  hashgt23el  14347  seqcoll  14387  hashle2pr  14400  elss2prb  14411  ccatalpha  14517  swrdsbslen  14588  swrdspsleq  14589  swrdswrdlem  14627  swrdswrd  14628  pfxccatin12lem2a  14650  pfxccatin12lem1  14651  pfxccatin12lem3  14655  swrdccat3blem  14662  reuccatpfxs1lem  14669  repswswrd  14707  cshf1  14733  swrd2lsw  14875  sqeqd  15089  sqrmo  15174  cau3lem  15278  icodiamlt  15361  limsupbnd2  15406  lo1bdd2  15447  climuni  15475  rlimcn3  15513  mulcn2  15519  o1of2  15536  rlimo1  15540  lo1le  15575  iseralt  15608  cvgrat  15806  fprodss  15871  rpnnen2lem12  16150  ruclem3  16158  sqrt2irr  16174  p1modz1  16186  dvdsmodexp  16187  dvds2lem  16195  dvdslelem  16236  dvdsabseq  16240  divalglem8  16327  bitsinv1lem  16368  sadcaddlem  16384  smu01lem  16412  smueqlem  16417  bezoutlem4  16469  dfgcd2  16473  algcvga  16506  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfdvdsb  16570  coprmgcdb  16576  coprmdvds2  16581  coprmprod  16588  isprm3  16610  prmdvdsfz  16632  isprm5  16634  coprm  16638  rpexp12i  16651  phibndlem  16697  dfphi2  16701  eulerthlem2  16709  odzdvds  16723  iserodd  16763  pclem  16766  pcpremul  16771  pcqcl  16784  pcdvdsb  16797  pcprmpw2  16810  difsqpwdvds  16815  pcaddlem  16816  pcmptcl  16819  pcfac  16827  prmpwdvds  16832  unbenlem  16836  prmreclem1  16844  4sqlem17  16889  vdwmc2  16907  vdwlem9  16917  vdwlem10  16918  vdwlem13  16921  vdwnnlem3  16925  ramcl  16957  prmgaplem7  16985  mreiincl  17515  initoid  17925  termoid  17926  initoeu2lem1  17938  pospo  18266  resspos  18352  resstos  18353  dirge  18526  cyccom  19132  gsmsymgrfixlem1  19356  oddvdsnn0  19473  oddvds  19476  odcl2  19494  gexdvds  19513  sylow2alem2  19547  sylow2a  19548  efgi2  19654  efgsrel  19663  efgs1b  19665  imasabl  19805  cyggex2  19826  telgsums  19922  pgpfac1lem2  20006  pgpfac1lem3a  20007  pgpfac1lem3  20008  pgpfac1lem5  20010  zrtermorngc  20576  zrtermoringc  20608  lmodfopnelem2  20850  lssssr  20905  rnglidlmcl  21171  gzrngunitlem  21387  znunit  21518  frgpcyg  21528  lsmcss  21647  obselocv  21683  obslbs  21685  mhpvarcl  22091  cply1mul  22240  gsummoncoe1  22252  cpmatacl  22660  cpmatinvcl  22661  cpmatmcllem  22662  m2cpminvid2lem  22698  mp2pm2mplem4  22753  pm2mp  22769  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmul0  22802  chfacfpmmul0  22806  cayhamlem4  22832  ordtrest2lem  23147  leordtval2  23156  lecldbas  23163  cncls  23218  cncnp  23224  cnpresti  23232  lmcnp  23248  cnt0  23290  isreg2  23321  cmpsublem  23343  cmpsub  23344  tgcmp  23345  bwth  23354  dfconn2  23363  1stcfb  23389  1stcelcls  23405  islly2  23428  dislly  23441  reftr  23458  comppfsc  23476  kgencn2  23501  txcnp  23564  txindis  23578  txcmplem1  23585  txlm  23592  xkohaus  23597  cnmptcom  23622  kqfvima  23674  isr0  23681  fgss2  23818  fbasrn  23828  filuni  23829  ufilmax  23851  isufil2  23852  cfinufil  23872  fmfnfmlem1  23898  fmfnfmlem2  23899  fmfnfmlem4  23901  fmfnfm  23902  fmco  23905  flimopn  23919  hausflim  23925  flimrest  23927  fclsopn  23958  flimfnfcls  23972  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALT  23995  ptcmplem2  23997  cnextcn  24011  symgtgp  24050  qustgplem  24065  tsmsres  24088  tsmsxplem1  24097  isucn2  24222  imasdsf1olem  24317  bldisj  24342  blssps  24368  blss  24369  metcnp3  24484  ngptgp  24580  nrginvrcn  24636  nmoleub  24675  xrsmopn  24757  icccmplem3  24769  reconnlem2  24772  rectbntr0  24777  rescncf  24846  iocopnst  24893  iccpnfcnv  24898  lebnumii  24921  nmoleub2lem  25070  nmhmcn  25076  iscfil3  25229  iscau2  25233  iscau3  25234  iscau4  25235  iscmet3lem2  25248  caussi  25253  equivcfil  25255  equivcau  25256  ivthlem2  25409  ivthlem3  25410  ovoliunlem2  25460  ovoliunnul  25464  ioombl1lem4  25518  dyadmax  25555  dyadmbl  25557  volsup2  25562  itg2le  25696  itg2const2  25698  itg2seq  25699  itgsplitioo  25795  rolle  25950  c1lip1  25958  dvivthlem1  25969  lhop1  25975  dvcnvrelem1  25978  dvfsumrlim  25994  ply1divmo  26097  ig1peu  26136  plypf1  26173  coeaddlem  26210  dvply2g  26248  fta1  26272  quotcan  26273  aalioulem4  26299  ulmcaulem  26359  ulmcn  26364  pilem2  26418  sincosq1lem  26462  sinq12gt0  26472  sinq12ge0  26473  tanord1  26502  lognegb  26555  logrec  26729  logbgcd1irr  26760  dcubic  26812  xrlimcnp  26934  o1cxp  26941  ftalem2  27040  ftalem3  27041  fsumdvdscom  27151  chtub  27179  vmasum  27183  bcmono  27244  bposlem3  27253  bposlem7  27257  lgsdir  27299  lgsqrlem2  27314  lgsqrmodndvds  27320  gausslemma2dlem6  27339  gausslemma2d  27341  lgsquadlem2  27348  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2sqlem6  27390  2sq2  27400  2sqmod  27403  dchrisumlem3  27458  pntrsumbnd2  27534  pntpbnd1  27553  pntibnd  27560  pntlem3  27576  pntleml  27578  ltsres  27630  nosepon  27633  nolesgn2o  27639  nogesgn1o  27641  nodenselem8  27659  nosupbnd1lem1  27676  madess  27862  madebdaylemlrcut  27895  peano5uzs  28400  bdayfinbndlem1  28463  z12bday  28481  brbtwn2  28978  colinearalg  28983  axcontlem10  29046  edgupgr  29207  edglnl  29216  usgruspgrb  29256  subupgr  29360  uhgrspan1  29376  usgredgsscusgredg  29533  fusgrn0degnn0  29573  upgrewlkle2  29680  uspgr2wlkeq  29719  redwlk  29744  wlkdlem2  29755  upgrwlkdvdelem  29809  pthdlem1  29839  pthdlem2  29841  crctcshwlkn0lem3  29885  wlkiswwlks1  29940  wwlksm1edg  29954  wwlksnred  29965  wwlksnextbi  29967  umgr2adedgspth  30021  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a  30073  clwlkclwwlkf1lem3  30081  clwwisshclwwslemlem  30088  clwwlkf  30122  clwwlkext2edg  30131  wwlksubclwwlk  30133  clwwlknonex2lem2  30183  eupth2lems  30313  frgrwopreglem4a  30385  frgrregorufrg  30401  ex-natded5.3-2  30483  isgrpo  30572  vacn  30769  ubthlem2  30946  htthlem  30992  normgt0  31202  shmodsi  31464  spansneleq  31645  h1datomi  31656  nmcexi  32101  pjnormssi  32243  stm1add3i  32322  golem2  32347  cvnsym  32365  dmdmd  32375  mdslmd1lem1  32400  mdslmd1i  32404  mdexchi  32410  atcveq0  32423  superpos  32429  hatomistici  32437  atoml2i  32458  atcvat2i  32462  chirredlem1  32465  atcvat3i  32471  mdsymlem3  32480  mdsymlem5  32482  cdj3lem2b  32512  cdj3i  32516  submarchi  33268  dfufd2  33631  tpr2rico  34069  ordtrest2NEWlem  34079  xrge0iifcnv  34090  omssubadd  34457  eulerpartlemb  34525  ballotlemfc0  34650  ballotlemfcc  34651  ftc2re  34755  fissorduni  35246  fineqvinfep  35281  loop1cycl  35331  subfacp1lem6  35379  iccllysconn  35444  cvmfolem  35473  satfsschain  35558  satfrel  35561  satfdm  35563  sat1el2xp  35573  satffunlem1lem1  35596  dmopab3rexdif  35599  satffunlem2lem2  35600  satffun  35603  fundmpss  35961  dfon2lem3  35977  dfon2lem6  35980  axextbdist  35992  dfrdg4  36145  5segofs  36200  cgrextend  36202  segconeu  36205  btwncomim  36207  btwnswapid  36211  btwnintr  36213  btwnexch3  36214  btwndiff  36221  ifscgr  36238  cgrxfr  36249  btwnxfr  36250  lineext  36270  brofs2  36271  linecgr  36275  lineid  36277  idinside  36278  endofsegid  36279  btwnconn1lem13  36293  btwnconn3  36297  finminlem  36512  nn0prpwlem  36516  cldbnd  36520  clsint2  36523  fnessref  36551  neibastop3  36556  fgmin  36564  onsuct0  36635  limsucncmpi  36639  bj-nnfea  36935  bj-axc14  37057  bj-restn0  37295  bj-0int  37306  wl-19.2reqv  37729  wl-aetr  37734  wl-axc11r  37735  fin2so  37808  tan2h  37813  lindsenlbs  37816  poimirlem2  37823  poimirlem9  37830  poimirlem17  37838  poimirlem18  37839  poimirlem21  37842  poimirlem23  37844  poimirlem26  37847  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimir  37854  heicant  37856  mblfinlem2  37859  mblfinlem3  37860  itg2addnclem  37872  itg2addnclem2  37873  itg2gt0cn  37876  ftc1anclem5  37898  ftc1anclem6  37899  filbcmb  37941  nninfnub  37952  mettrifi  37958  geomcau  37960  istotbnd3  37972  sstotbnd2  37975  ismtybndlem  38007  heibor1lem  38010  heiborlem1  38012  heiborlem8  38019  heiborlem10  38021  heibor  38022  opidonOLD  38053  riscer  38189  crngohomfo  38207  keridl  38233  ispridl2  38239  ispridlc  38271  ac6s6  38373  eqvreltr  38864  dral1-o  39164  ax12indalem  39205  ax12inda2ALT  39206  lsatcveq0  39292  eqlkr3  39361  atlatmstc  39579  atlrelat1  39581  hlrelat2  39663  intnatN  39667  cvrexchlem  39679  cvratlem  39681  cvrat2  39689  atltcvr  39695  cvrat3  39702  cvrat4  39703  ps-1  39737  ps-2  39738  lplnnle2at  39801  lvolnle3at  39842  2llnma3r  40048  cdlemblem  40053  pmapjoin  40112  elpcliN  40153  lhpmcvr4N  40286  4atexlemnclw  40330  trlnidatb  40437  cdlemc4  40454  cdlemd3  40460  cdleme3g  40494  cdleme7d  40506  cdleme11c  40521  cdleme11dN  40522  cdleme21b  40586  cdleme21c  40587  cdleme21i  40595  cdleme22b  40601  cdleme35fnpq  40709  cdlemf1  40821  trlord  40829  cdlemg6c  40880  dihglblem6  41600  dochlkr  41645  dochkrshp  41646  dihjat1lem  41688  dochexmidlem5  41724  dochexmidlem8  41727  qsalrel  42496  remulcand  42694  prjspner1  42869  fphpdo  43059  pellexlem5  43075  pellexlem6  43076  jm2.26lem3  43243  unxpwdom3  43337  omlimcl2  43484  oe0suclim  43519  cantnfresb  43566  tfsconcatb0  43586  naddgeoa  43636  iscard5  43777  sqrtcval  43882  ov2ssiunov2  43941  frege124d  44002  ordpss  44691  19.41rg  44791  relpfrlem  45194  modelaxreplem2  45220  stoweidlem34  46278  ormklocald  47118  evenwodadd  47131  cfsetsnfsetf1  47305  fcoresf1  47315  euoreqb  47355  2reu8i  47359  ralralimp  47524  f1oresf1o2  47537  zm1nn  47548  elfz2z  47561  2tceilhalfelfzo1  47578  m1modmmod  47604  modlt0b  47609  iccpartlt  47670  iccelpart  47679  icceuelpartlem  47681  fargshiftf1  47687  sprsymrelf1lem  47737  paireqne  47757  reuopreuprim  47772  goldbachthlem2  47792  odz2prm2pw  47809  fmtnoprmfac1lem  47810  fmtnofac2lem  47814  prmdvdsfmtnof1  47833  sfprmdvdsmersenne  47849  lighneallem2  47852  lighneallem4  47856  fppr2odd  47977  gbegt5  48007  gbowge7  48009  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgoldbach  48063  grimuhgr  48133  grimcnv  48134  grimco  48135  isuspgrim0  48140  isuspgrimlem  48141  upgrimwlklem5  48147  upgrimtrlslem2  48151  uhgrimisgrgriclem  48176  clnbgrgrimlem  48179  clnbgrgrim  48180  grimedg  48181  grtriprop  48187  isubgr3stgrlem3  48214  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  uspgrlimlem3  48236  grlimedgclnbgr  48241  grlimgrtrilem2  48248  grlimgrtri  48249  grlicsym  48259  gpgedgvtx1  48308  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  lcosslsp  48684  lindslinindsimp1  48703  snlindsntor  48717  itcovalt2  48923  eenglngeehlnmlem2  48984  itsclc0yqsol  49010  itschlc0xyqsol1  49012  itschlc0xyqsol  49013  opnneilv  49154  i0oii  49165  io1ii  49166  iscnrm3lem4  49181  iscnrm3r  49193  setrec1lem4  49935  aacllem  50046