Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30428 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  2176  alrimdd  2211  axc16g  2257  axc16nf  2260  axc11r  2368  sb4a  2482  2eu1  2648  2eu1v  2649  ss2ralv  4065  ss2rexv  4066  trel3  5274  poss  5598  sess2  5654  wefrc  5682  wereu2  5685  predtrss  6344  frpomin  6362  funun  6613  ssimaex  6993  f1cofveqaeq  7277  f1imass  7283  soisoi  7347  isores3  7354  isofrlem  7359  isoselem  7360  weniso  7373  abnexg  7774  oninton  7814  orduniorsuc  7849  limuni3  7872  tfindsg  7881  limom  7902  f1o2ndf1  8145  soxp  8152  xpord3inddlem  8177  soseq  8182  extmptsuppeq  8211  smoel  8398  tfrlem9  8423  tz7.49  8483  seqomlem1  8488  odi  8615  omass  8616  omeulem2  8619  oeordsuc  8630  oeeulem  8637  naddsuc2  8737  ertr  8758  swoord2  8776  ecopovtrn  8858  domtriord  9161  pssnn  9206  onomeneqOLD  9263  unxpdomlem2  9284  isinf  9293  isinfOLD  9294  f1finf1o  9302  findcard3  9315  findcard3OLD  9316  frfi  9318  unblem3  9327  en3lplem1  9649  inf3lem5  9669  cantnfle  9708  cantnfp1lem3  9717  ttrcltr  9753  frmin  9786  rankxpsuc  9919  tcrank  9921  ficardom  9998  carduni  10018  infxpenlem  10050  dfac8alem  10066  ac10ct  10071  ween  10072  alephdom  10118  alephle  10125  iscard3  10130  alephfp  10145  pwsdompw  10240  infdif  10245  cfslbn  10304  cofsmo  10306  cfcof  10311  fin1a2s  10451  domtriomlem  10479  ac6num  10516  zorn2lem3  10535  axdclem2  10557  imadomg  10571  iundom2g  10577  ficard  10602  fpwwe2lem7  10674  fpwwe2  10680  gchpwdom  10707  gchaclem  10715  tskr1om2  10805  inar1  10812  tskord  10817  tskuni  10820  grudomon  10854  grur1a  10856  grur1  10857  addnidpi  10938  ltexnq  11012  genpnnp  11042  addclprlem2  11054  mulclprlem  11056  psslinpr  11068  ltexprlem6  11078  ltexprlem7  11079  addcanpr  11083  mulgt0sr  11142  map2psrpr  11147  supsrlem  11148  axrrecex  11200  letr  11352  dedekind  11421  recex  11892  lemul12b  12121  mulgt1OLD  12123  fimaxre2  12210  lbreu  12215  nnrecgt0  12306  nnunb  12519  bndndx  12522  zeo  12701  uzind  12707  fzind  12713  fnn0ind  12714  suprfinzcl  12729  suprzcl2  12977  zmax  12984  rpnnen1lem5  13020  xrletr  13196  qbtwnre  13237  qsqueeze  13239  qextltlem  13240  xralrple  13243  xlesubadd  13301  supxrunb1  13357  icoshft  13509  zltaddlt1le  13541  fzen  13577  elfz0fzfz0  13669  elfzmlbp  13675  elfzo0z  13737  fzofzim  13745  fzo1fzo0n0  13750  elfzodifsumelfzo  13766  ssfzoulel  13795  modadd1  13944  modmul1  13961  uzrdgfni  13995  fsuppmapnn0fiub0  14030  fsuppmapnn0ub  14032  fsuppmapnn0fz  14033  seqf1olem1  14078  seqf1olem2  14079  expnbnd  14267  faclbnd4lem4  14331  hashgt23el  14459  seqcoll  14499  hashle2pr  14512  elss2prb  14523  ccatalpha  14627  swrdsbslen  14698  swrdspsleq  14699  swrdswrdlem  14738  swrdswrd  14739  pfxccatin12lem2a  14761  pfxccatin12lem1  14762  pfxccatin12lem3  14766  swrdccat3blem  14773  reuccatpfxs1lem  14780  repswswrd  14818  cshf1  14844  swrd2lsw  14987  sqeqd  15201  sqrmo  15286  cau3lem  15389  icodiamlt  15470  limsupbnd2  15515  lo1bdd2  15556  climuni  15584  rlimcn3  15622  mulcn2  15628  o1of2  15645  rlimo1  15649  lo1le  15684  iseralt  15717  cvgrat  15915  fprodss  15980  rpnnen2lem12  16257  ruclem3  16265  sqrt2irr  16281  p1modz1  16293  dvdsmodexp  16294  dvds2lem  16302  dvdslelem  16342  dvdsabseq  16346  divalglem8  16433  bitsinv1lem  16474  sadcaddlem  16490  smu01lem  16518  smueqlem  16523  bezoutlem4  16575  dfgcd2  16579  algcvga  16612  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfdvdsb  16676  coprmgcdb  16682  coprmdvds2  16687  coprmprod  16694  isprm3  16716  prmdvdsfz  16738  isprm5  16740  coprm  16744  rpexp12i  16757  phibndlem  16803  dfphi2  16807  eulerthlem2  16815  odzdvds  16828  iserodd  16868  pclem  16871  pcpremul  16876  pcqcl  16889  pcdvdsb  16902  pcprmpw2  16915  difsqpwdvds  16920  pcaddlem  16921  pcmptcl  16924  pcfac  16932  prmpwdvds  16937  unbenlem  16941  prmreclem1  16949  4sqlem17  16994  vdwmc2  17012  vdwlem9  17022  vdwlem10  17023  vdwlem13  17026  vdwnnlem3  17030  ramcl  17062  prmgaplem7  17090  mreiincl  17640  initoid  18054  termoid  18055  initoeu2lem1  18067  pospo  18402  dirge  18660  cyccom  19233  gsmsymgrfixlem1  19459  oddvdsnn0  19576  oddvds  19579  odcl2  19597  gexdvds  19616  sylow2alem2  19650  sylow2a  19651  efgi2  19757  efgsrel  19766  efgs1b  19768  imasabl  19908  cyggex2  19929  telgsums  20025  pgpfac1lem2  20109  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfac1lem5  20113  zrtermorngc  20659  zrtermoringc  20691  lmodfopnelem2  20913  lssssr  20969  rnglidlmcl  21243  gzrngunitlem  21467  znunit  21599  frgpcyg  21609  lsmcss  21727  obselocv  21765  obslbs  21767  mhpvarcl  22169  cply1mul  22315  gsummoncoe1  22327  cpmatacl  22737  cpmatinvcl  22738  cpmatmcllem  22739  m2cpminvid2lem  22775  mp2pm2mplem4  22830  pm2mp  22846  chfacfisf  22875  chfacfisfcpmat  22876  chfacfscmul0  22879  chfacfpmmul0  22883  cayhamlem4  22909  ordtrest2lem  23226  leordtval2  23235  lecldbas  23242  cncls  23297  cncnp  23303  cnpresti  23311  lmcnp  23327  cnt0  23369  isreg2  23400  cmpsublem  23422  cmpsub  23423  tgcmp  23424  bwth  23433  dfconn2  23442  1stcfb  23468  1stcelcls  23484  islly2  23507  dislly  23520  reftr  23537  comppfsc  23555  kgencn2  23580  txcnp  23643  txindis  23657  txcmplem1  23664  txlm  23671  xkohaus  23676  cnmptcom  23701  kqfvima  23753  isr0  23760  fgss2  23897  fbasrn  23907  filuni  23908  ufilmax  23930  isufil2  23931  cfinufil  23951  fmfnfmlem1  23977  fmfnfmlem2  23978  fmfnfmlem4  23980  fmfnfm  23981  fmco  23984  flimopn  23998  hausflim  24004  flimrest  24006  fclsopn  24037  flimfnfcls  24051  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALT  24074  ptcmplem2  24076  cnextcn  24090  symgtgp  24129  qustgplem  24144  tsmsres  24167  tsmsxplem1  24176  isucn2  24303  imasdsf1olem  24398  bldisj  24423  blssps  24449  blss  24450  metcnp3  24568  ngptgp  24664  nrginvrcn  24728  nmoleub  24767  xrsmopn  24847  icccmplem3  24859  reconnlem2  24862  rectbntr0  24867  rescncf  24936  iocopnst  24983  iccpnfcnv  24988  lebnumii  25011  nmoleub2lem  25160  nmhmcn  25166  iscfil3  25320  iscau2  25324  iscau3  25325  iscau4  25326  iscmet3lem2  25339  caussi  25344  equivcfil  25346  equivcau  25347  ivthlem2  25500  ivthlem3  25501  ovoliunlem2  25551  ovoliunnul  25555  ioombl1lem4  25609  dyadmax  25646  dyadmbl  25648  volsup2  25653  itg2le  25788  itg2const2  25790  itg2seq  25791  itgsplitioo  25887  rolle  26042  c1lip1  26050  dvivthlem1  26061  lhop1  26067  dvcnvrelem1  26070  dvfsumrlim  26086  ply1divmo  26189  ig1peu  26228  plypf1  26265  coeaddlem  26302  dvply2g  26340  fta1  26364  quotcan  26365  aalioulem4  26391  ulmcaulem  26451  ulmcn  26456  pilem2  26510  sincosq1lem  26553  sinq12gt0  26563  sinq12ge0  26564  tanord1  26593  lognegb  26646  logrec  26820  logbgcd1irr  26851  dcubic  26903  xrlimcnp  27025  o1cxp  27032  ftalem2  27131  ftalem3  27132  fsumdvdscom  27242  chtub  27270  vmasum  27274  bcmono  27335  bposlem3  27344  bposlem7  27348  lgsdir  27390  lgsqrlem2  27405  lgsqrmodndvds  27411  gausslemma2dlem6  27430  gausslemma2d  27432  lgsquadlem2  27439  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgslem3d1  27461  2sqlem6  27481  2sq2  27491  2sqmod  27494  dchrisumlem3  27549  pntrsumbnd2  27625  pntpbnd1  27644  pntibnd  27651  pntlem3  27667  pntleml  27669  sltres  27721  nosepon  27724  nolesgn2o  27730  nogesgn1o  27732  nodenselem8  27750  nosupbnd1lem1  27767  madess  27929  madebdaylemlrcut  27951  peano5uzs  28404  brbtwn2  28934  colinearalg  28939  axcontlem10  29002  edgupgr  29165  edglnl  29174  usgruspgrb  29214  subupgr  29318  uhgrspan1  29334  usgredgsscusgredg  29491  fusgrn0degnn0  29531  upgrewlkle2  29638  uspgr2wlkeq  29678  redwlk  29704  wlkdlem2  29715  upgrwlkdvdelem  29768  pthdlem1  29798  pthdlem2  29800  crctcshwlkn0lem3  29841  wlkiswwlks1  29896  wwlksm1edg  29910  wwlksnred  29921  wwlksnextbi  29923  umgr2adedgspth  29977  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a  30026  clwlkclwwlkf1lem3  30034  clwwisshclwwslemlem  30041  clwwlkf  30075  clwwlkext2edg  30084  wwlksubclwwlk  30086  clwwlknonex2lem2  30136  eupth2lems  30266  frgrwopreglem4a  30338  frgrregorufrg  30354  ex-natded5.3-2  30436  isgrpo  30525  vacn  30722  ubthlem2  30899  htthlem  30945  normgt0  31155  shmodsi  31417  spansneleq  31598  h1datomi  31609  nmcexi  32054  pjnormssi  32196  stm1add3i  32275  golem2  32300  cvnsym  32318  dmdmd  32328  mdslmd1lem1  32353  mdslmd1i  32357  mdexchi  32363  atcveq0  32376  superpos  32382  hatomistici  32390  atoml2i  32411  atcvat2i  32415  chirredlem1  32418  atcvat3i  32424  mdsymlem3  32433  mdsymlem5  32435  cdj3lem2b  32465  cdj3i  32469  supssd  32726  infssd  32727  resspos  32940  resstos  32941  submarchi  33175  dfufd2  33557  tpr2rico  33872  ordtrest2NEWlem  33882  xrge0iifcnv  33893  omssubadd  34281  eulerpartlemb  34349  ballotlemfc0  34473  ballotlemfcc  34474  ftc2re  34591  loop1cycl  35121  subfacp1lem6  35169  iccllysconn  35234  cvmfolem  35263  satfsschain  35348  satfrel  35351  satfdm  35353  sat1el2xp  35363  satffunlem1lem1  35386  dmopab3rexdif  35389  satffunlem2lem2  35390  satffun  35393  fundmpss  35747  dfon2lem3  35766  dfon2lem6  35769  axextbdist  35781  dfrdg4  35932  5segofs  35987  cgrextend  35989  segconeu  35992  btwncomim  35994  btwnswapid  35998  btwnintr  36000  btwnexch3  36001  btwndiff  36008  ifscgr  36025  cgrxfr  36036  btwnxfr  36037  lineext  36057  brofs2  36058  linecgr  36062  lineid  36064  idinside  36065  endofsegid  36066  btwnconn1lem13  36080  btwnconn3  36084  finminlem  36300  nn0prpwlem  36304  cldbnd  36308  clsint2  36311  fnessref  36339  neibastop3  36344  fgmin  36352  onsuct0  36423  limsucncmpi  36427  bj-nnfea  36716  bj-axc14  36838  bj-restn0  37072  bj-0int  37083  wl-19.2reqv  37504  wl-aetr  37509  wl-axc11r  37510  fin2so  37593  tan2h  37598  lindsenlbs  37601  poimirlem2  37608  poimirlem9  37615  poimirlem17  37623  poimirlem18  37624  poimirlem21  37627  poimirlem23  37629  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimir  37639  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  itg2addnclem  37657  itg2addnclem2  37658  itg2gt0cn  37661  ftc1anclem5  37683  ftc1anclem6  37684  filbcmb  37726  nninfnub  37737  mettrifi  37743  geomcau  37745  istotbnd3  37757  sstotbnd2  37760  ismtybndlem  37792  heibor1lem  37795  heiborlem1  37797  heiborlem8  37804  heiborlem10  37806  heibor  37807  opidonOLD  37838  riscer  37974  crngohomfo  37992  keridl  38018  ispridl2  38024  ispridlc  38056  ac6s6  38158  eqvreltr  38588  dral1-o  38885  ax12indalem  38926  ax12inda2ALT  38927  lsatcveq0  39013  eqlkr3  39082  atlatmstc  39300  atlrelat1  39302  hlrelat2  39385  intnatN  39389  cvrexchlem  39401  cvratlem  39403  cvrat2  39411  atltcvr  39417  cvrat3  39424  cvrat4  39425  ps-1  39459  ps-2  39460  lplnnle2at  39523  lvolnle3at  39564  2llnma3r  39770  cdlemblem  39775  pmapjoin  39834  elpcliN  39875  lhpmcvr4N  40008  4atexlemnclw  40052  trlnidatb  40159  cdlemc4  40176  cdlemd3  40182  cdleme3g  40216  cdleme7d  40228  cdleme11c  40243  cdleme11dN  40244  cdleme21b  40308  cdleme21c  40309  cdleme21i  40317  cdleme22b  40323  cdleme35fnpq  40431  cdlemf1  40543  trlord  40551  cdlemg6c  40602  dihglblem6  41322  dochlkr  41367  dochkrshp  41368  dihjat1lem  41410  dochexmidlem5  41446  dochexmidlem8  41449  metakunt29  42214  qsalrel  42259  remulcand  42444  prjspner1  42612  fphpdo  42804  pellexlem5  42820  pellexlem6  42821  jm2.26lem3  42989  unxpwdom3  43083  omlimcl2  43230  oe0suclim  43266  cantnfresb  43313  tfsconcatb0  43333  naddgeoa  43383  iscard5  43525  sqrtcval  43630  ov2ssiunov2  43689  frege124d  43750  ordpss  44446  19.41rg  44547  modelaxreplem2  44943  stoweidlem34  45989  cfsetsnfsetf1  47008  fcoresf1  47018  euoreqb  47058  2reu8i  47062  ralralimp  47227  f1oresf1o2  47240  zm1nn  47251  elfz2z  47264  iccpartlt  47348  iccelpart  47357  icceuelpartlem  47359  fargshiftf1  47365  sprsymrelf1lem  47415  paireqne  47435  reuopreuprim  47450  goldbachthlem2  47470  odz2prm2pw  47487  fmtnoprmfac1lem  47488  fmtnofac2lem  47492  prmdvdsfmtnof1  47511  sfprmdvdsmersenne  47527  lighneallem2  47530  lighneallem4  47534  fppr2odd  47655  gbegt5  47685  gbowge7  47687  bgoldbtbndlem4  47732  bgoldbtbnd  47733  tgoldbach  47741  isuspgrim0  47809  isuspgrimlem  47811  grimuhgr  47815  grimcnv  47816  grimco  47817  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840  grtriprop  47845  isubgr3stgrlem3  47870  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  uspgrlimlem3  47892  grlimgrtrilem2  47897  grlimgrtri  47898  grlicsym  47908  2tceilhalfelfzo1  47952  gpgedgvtx1  47954  lcosslsp  48283  lindslinindsimp1  48302  snlindsntor  48316  m1modmmod  48370  itcovalt2  48526  eenglngeehlnmlem2  48587  itsclc0yqsol  48613  itschlc0xyqsol1  48615  itschlc0xyqsol  48616  opnneilv  48704  i0oii  48715  io1ii  48716  iscnrm3lem4  48732  iscnrm3r  48744  setrec1lem4  48920  aacllem  49031