Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 28179 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  181  sylibd  241  sylbid  242  sylibrd  261  sylbird  262  syland  604  animpimp2impd  842  ax12v2  2179  alrimdd  2214  axc16g  2261  axc16nf  2264  axc11r  2386  sb1OLD  2507  sb4a  2509  sbequiOLD  2534  sbequiALT  2596  2eu1  2735  2eu1v  2736  ss2ralv  4035  ss2rexv  4036  trel3  5180  poss  5476  sess2  5524  wefrc  5549  wereu2  5552  funun  6400  ssimaex  6748  f1cofveqaeq  7016  f1imass  7022  soisoi  7081  isores3  7088  isofrlem  7093  isoselem  7094  weniso  7107  abnexg  7478  oninton  7515  orduniorsuc  7545  limuni3  7567  tfindsg  7575  limom  7595  f1o2ndf1  7818  soxp  7823  extmptsuppeq  7854  smoel  7997  tfrlem9  8021  tz7.49  8081  seqomlem1  8086  odi  8205  omass  8206  omeulem2  8209  oeordsuc  8220  oeeulem  8227  ertr  8304  swoord2  8321  ecopovtrn  8400  domtriord  8663  onomeneq  8708  unxpdomlem2  8723  isinf  8731  pssnn  8736  findcard3  8761  frfi  8763  unblem3  8772  en3lplem1  9075  inf3lem5  9095  cantnfle  9134  cantnfp1lem3  9143  rankxpsuc  9311  tcrank  9313  ficardom  9390  carduni  9410  infxpenlem  9439  dfac8alem  9455  ac10ct  9460  ween  9461  alephdom  9507  alephle  9514  iscard3  9519  alephfp  9534  pwsdompw  9626  infdif  9631  cfslbn  9689  cofsmo  9691  cfcof  9696  fin1a2s  9836  domtriomlem  9864  ac6num  9901  zorn2lem3  9920  axdclem2  9942  imadomg  9956  iundom2g  9962  ficard  9987  fpwwe2lem8  10059  fpwwe2  10065  gchpwdom  10092  gchaclem  10100  tskr1om2  10190  inar1  10197  tskord  10202  tskuni  10205  grudomon  10239  grur1a  10241  grur1  10242  addnidpi  10323  ltexnq  10397  genpnnp  10427  addclprlem2  10439  mulclprlem  10441  psslinpr  10453  ltexprlem6  10463  ltexprlem7  10464  addcanpr  10468  mulgt0sr  10527  map2psrpr  10532  supsrlem  10533  axrrecex  10585  letr  10734  dedekind  10803  recex  11272  lemul12b  11497  mulgt1  11499  fimaxre2  11586  lbreu  11591  nnrecgt0  11681  nnunb  11894  bndndx  11897  zeo  12069  uzind  12075  fzind  12081  fnn0ind  12082  suprfinzcl  12098  suprzcl2  12339  zmax  12346  rpnnen1lem5  12381  xrletr  12552  qbtwnre  12593  qsqueeze  12595  qextltlem  12596  xralrple  12599  xlesubadd  12657  supxrunb1  12713  icoshft  12860  zltaddlt1le  12891  fzen  12925  elfz0fzfz0  13013  elfzmlbp  13019  elfzo0z  13080  fzofzim  13085  fzo1fzo0n0  13089  elfzodifsumelfzo  13104  ssfzoulel  13132  modadd1  13277  modmul1  13293  uzrdgfni  13327  fsuppmapnn0fiub0  13362  fsuppmapnn0ub  13364  fsuppmapnn0fz  13365  seqf1olem1  13410  seqf1olem2  13411  expnbnd  13594  faclbnd4lem4  13657  hashgt23el  13786  seqcoll  13823  hashle2pr  13836  elss2prb  13846  ccatalpha  13947  swrdsbslen  14026  swrdspsleq  14027  swrdswrdlem  14066  swrdswrd  14067  pfxccatin12lem2a  14089  pfxccatin12lem1  14090  pfxccatin12lem3  14094  swrdccat3blem  14101  reuccatpfxs1lem  14108  repswswrd  14146  cshf1  14172  swrd2lsw  14314  sqeqd  14525  sqrmo  14611  cau3lem  14714  icodiamlt  14795  limsupbnd2  14840  lo1bdd2  14881  climuni  14909  rlimcn2  14947  mulcn2  14952  o1of2  14969  rlimo1  14973  lo1le  15008  iseralt  15041  cvgrat  15239  fprodss  15302  rpnnen2lem12  15578  ruclem3  15586  sqrt2irr  15602  p1modz1  15614  dvdsmodexp  15615  dvds2lem  15622  dvdslelem  15659  dvdsabseq  15663  divalglem8  15751  bitsinv1lem  15790  sadcaddlem  15806  smu01lem  15834  smueqlem  15839  bezoutlem4  15890  dfgcd2  15894  algcvga  15923  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfdvdsb  15987  coprmgcdb  15993  coprmdvds2  15998  coprmprod  16005  isprm3  16027  prmdvdsfz  16049  isprm5  16051  coprm  16055  rpexp12i  16066  phibndlem  16107  dfphi2  16111  eulerthlem2  16119  odzdvds  16132  iserodd  16172  pclem  16175  pcpremul  16180  pcqcl  16193  pcdvdsb  16205  pcprmpw2  16218  difsqpwdvds  16223  pcaddlem  16224  pcmptcl  16227  pcfac  16235  prmpwdvds  16240  unbenlem  16244  prmreclem1  16252  4sqlem17  16297  vdwmc2  16315  vdwlem9  16325  vdwlem10  16326  vdwlem13  16329  vdwnnlem3  16333  ramcl  16365  prmgaplem7  16393  mreiincl  16867  initoid  17265  termoid  17266  initoeu2lem1  17274  pospo  17583  dirge  17847  cyccom  18346  gsmsymgrfixlem1  18555  oddvdsnn0  18672  oddvds  18675  odcl2  18692  gexdvds  18709  sylow2alem2  18743  sylow2a  18744  efgi2  18851  efgsrel  18860  efgs1b  18862  cyggex2  19017  telgsums  19113  pgpfac1lem2  19197  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfac1lem5  19201  lmodfopnelem2  19671  lssssr  19725  cply1mul  20462  gsummoncoe1  20472  gzrngunitlem  20610  znunit  20710  frgpcyg  20720  lsmcss  20836  obselocv  20872  obslbs  20874  cpmatacl  21324  cpmatinvcl  21325  cpmatmcllem  21326  m2cpminvid2lem  21362  mp2pm2mplem4  21417  pm2mp  21433  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmul0  21466  chfacfpmmul0  21470  cayhamlem4  21496  ordtrest2lem  21811  leordtval2  21820  lecldbas  21827  cncls  21882  cncnp  21888  cnpresti  21896  lmcnp  21912  cnt0  21954  isreg2  21985  cmpsublem  22007  cmpsub  22008  tgcmp  22009  bwth  22018  dfconn2  22027  1stcfb  22053  1stcelcls  22069  islly2  22092  dislly  22105  reftr  22122  comppfsc  22140  kgencn2  22165  txcnp  22228  txindis  22242  txcmplem1  22249  txlm  22256  xkohaus  22261  cnmptcom  22286  kqfvima  22338  isr0  22345  fgss2  22482  fbasrn  22492  filuni  22493  ufilmax  22515  isufil2  22516  cfinufil  22536  fmfnfmlem1  22562  fmfnfmlem2  22563  fmfnfmlem4  22565  fmfnfm  22566  fmco  22569  flimopn  22583  hausflim  22589  flimrest  22591  fclsopn  22622  flimfnfcls  22636  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALT  22659  ptcmplem2  22661  cnextcn  22675  symgtgp  22714  qustgplem  22729  tsmsres  22752  tsmsxplem1  22761  isucn2  22888  imasdsf1olem  22983  bldisj  23008  blssps  23034  blss  23035  metcnp3  23150  ngptgp  23245  nrginvrcn  23301  nmoleub  23340  xrsmopn  23420  icccmplem3  23432  reconnlem2  23435  rectbntr0  23440  rescncf  23505  iocopnst  23544  iccpnfcnv  23548  lebnumii  23570  nmoleub2lem  23718  nmhmcn  23724  iscfil3  23876  iscau2  23880  iscau3  23881  iscau4  23882  iscmet3lem2  23895  caussi  23900  equivcfil  23902  equivcau  23903  ivthlem2  24053  ivthlem3  24054  ovoliunlem2  24104  ovoliunnul  24108  ioombl1lem4  24162  dyadmax  24199  dyadmbl  24201  volsup2  24206  itg2le  24340  itg2const2  24342  itg2seq  24343  itgsplitioo  24438  rolle  24587  c1lip1  24594  dvivthlem1  24605  lhop1  24611  dvcnvrelem1  24614  dvfsumrlim  24628  ply1divmo  24729  ig1peu  24765  plypf1  24802  coeaddlem  24839  fta1  24897  quotcan  24898  aalioulem4  24924  ulmcaulem  24982  ulmcn  24987  pilem2  25040  sincosq1lem  25083  sinq12gt0  25093  sinq12ge0  25094  tanord1  25121  lognegb  25173  logrec  25341  logbgcd1irr  25372  dcubic  25424  xrlimcnp  25546  o1cxp  25552  ftalem2  25651  ftalem3  25652  fsumdvdscom  25762  chtub  25788  vmasum  25792  bcmono  25853  bposlem3  25862  bposlem7  25866  lgsdir  25908  lgsqrlem2  25923  lgsqrmodndvds  25929  gausslemma2dlem6  25948  gausslemma2d  25950  lgsquadlem2  25957  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2sqlem6  25999  2sq2  26009  2sqmod  26012  dchrisumlem3  26067  pntrsumbnd2  26143  pntpbnd1  26162  pntibnd  26169  pntlem3  26185  pntleml  26187  brbtwn2  26691  colinearalg  26696  axcontlem10  26759  edgupgr  26919  edglnl  26928  usgruspgrb  26966  subupgr  27069  uhgrspan1  27085  usgredgsscusgredg  27241  fusgrn0degnn0  27281  upgrewlkle2  27388  uspgr2wlkeq  27427  redwlk  27454  wlkdlem2  27465  upgrwlkdvdelem  27517  pthdlem1  27547  pthdlem2  27549  crctcshwlkn0lem3  27590  wlkiswwlks1  27645  wwlksm1edg  27659  wwlksnred  27670  wwlksnextbi  27672  umgr2adedgspth  27727  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a  27776  clwlkclwwlkf1lem3  27784  clwwisshclwwslemlem  27791  clwwlkf  27826  clwwlkext2edg  27835  wwlksubclwwlk  27837  clwwlknonex2lem2  27887  eupth2lems  28017  frgrwopreglem4a  28089  frgrregorufrg  28105  ex-natded5.3-2  28187  isgrpo  28274  vacn  28471  ubthlem2  28648  htthlem  28694  normgt0  28904  shmodsi  29166  spansneleq  29347  h1datomi  29358  nmcexi  29803  pjnormssi  29945  stm1add3i  30024  golem2  30049  cvnsym  30067  dmdmd  30077  mdslmd1lem1  30102  mdslmd1i  30106  mdexchi  30112  atcveq0  30125  superpos  30131  hatomistici  30139  atoml2i  30160  atcvat2i  30164  chirredlem1  30167  atcvat3i  30173  mdsymlem3  30182  mdsymlem5  30184  cdj3lem2b  30214  cdj3i  30218  supssd  30445  infssd  30446  resspos  30646  resstos  30647  submarchi  30815  tpr2rico  31155  ordtrest2NEWlem  31165  xrge0iifcnv  31176  omssubadd  31558  eulerpartlemb  31626  ballotlemfc0  31750  ballotlemfcc  31751  ftc2re  31869  loop1cycl  32384  subfacp1lem6  32432  iccllysconn  32497  cvmfolem  32526  satfsschain  32611  satfrel  32614  satfdm  32616  sat1el2xp  32626  satffunlem1lem1  32649  dmopab3rexdif  32652  satffunlem2lem2  32653  satffun  32656  fundmpss  33009  dfon2lem3  33030  dfon2lem6  33033  axextbdist  33045  trpredtr  33069  trpredmintr  33070  dftrpred3g  33072  trpredrec  33077  frpomin  33078  frmin  33084  soseq  33096  sltres  33169  nosepon  33172  nolesgn2o  33178  nodenselem8  33195  nosupbnd1lem1  33208  dfrdg4  33412  5segofs  33467  cgrextend  33469  segconeu  33472  btwncomim  33474  btwnswapid  33478  btwnintr  33480  btwnexch3  33481  btwndiff  33488  ifscgr  33505  cgrxfr  33516  btwnxfr  33517  lineext  33537  brofs2  33538  linecgr  33542  lineid  33544  idinside  33545  endofsegid  33546  btwnconn1lem13  33560  btwnconn3  33564  finminlem  33666  nn0prpwlem  33670  cldbnd  33674  clsint2  33677  fnessref  33705  neibastop3  33710  fgmin  33718  onsuct0  33789  limsucncmpi  33793  bj-nnfea  34064  bj-axc14  34180  bj-restn0  34384  bj-0int  34396  wl-19.2reqv  34779  wl-aetr  34784  wl-axc11r  34785  fin2so  34894  tan2h  34899  lindsenlbs  34902  poimirlem2  34909  poimirlem9  34916  poimirlem17  34924  poimirlem18  34925  poimirlem21  34928  poimirlem23  34930  poimirlem26  34933  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimir  34940  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  itg2addnclem  34958  itg2addnclem2  34959  itg2gt0cn  34962  ftc1anclem5  34986  ftc1anclem6  34987  filbcmb  35030  nninfnub  35041  mettrifi  35047  geomcau  35049  istotbnd3  35064  sstotbnd2  35067  ismtybndlem  35099  heibor1lem  35102  heiborlem1  35104  heiborlem8  35111  heiborlem10  35113  heibor  35114  opidonOLD  35145  riscer  35281  crngohomfo  35299  keridl  35325  ispridl2  35331  ispridlc  35363  ac6s6  35465  eqvreltr  35857  dral1-o  36055  ax12indalem  36096  ax12inda2ALT  36097  lsatcveq0  36183  eqlkr3  36252  atlatmstc  36470  atlrelat1  36472  hlrelat2  36554  intnatN  36558  cvrexchlem  36570  cvratlem  36572  cvrat2  36580  atltcvr  36586  cvrat3  36593  cvrat4  36594  ps-1  36628  ps-2  36629  lplnnle2at  36692  lvolnle3at  36733  2llnma3r  36939  cdlemblem  36944  pmapjoin  37003  elpcliN  37044  lhpmcvr4N  37177  4atexlemnclw  37221  trlnidatb  37328  cdlemc4  37345  cdlemd3  37351  cdleme3g  37385  cdleme7d  37397  cdleme11c  37412  cdleme11dN  37413  cdleme21b  37477  cdleme21c  37478  cdleme21i  37486  cdleme22b  37492  cdleme35fnpq  37600  cdlemf1  37712  trlord  37720  cdlemg6c  37771  dihglblem6  38491  dochlkr  38536  dochkrshp  38537  dihjat1lem  38579  dochexmidlem5  38615  dochexmidlem8  38618  qsalrel  39145  remulcand  39270  fphpdo  39434  pellexlem5  39450  pellexlem6  39451  jm2.26lem3  39618  unxpwdom3  39715  iscard5  39921  ov2ssiunov2  40065  frege124d  40126  ordpss  40803  19.41rg  40904  stoweidlem34  42339  euoreqb  43328  2reu8i  43332  ralralimp  43497  f1oresf1o2  43510  zm1nn  43522  elfz2z  43535  iccpartlt  43604  iccelpart  43613  icceuelpartlem  43615  fargshiftf1  43621  sprsymrelf1lem  43673  paireqne  43693  reuopreuprim  43708  goldbachthlem2  43728  odz2prm2pw  43745  fmtnoprmfac1lem  43746  fmtnofac2lem  43750  prmdvdsfmtnof1  43769  sfprmdvdsmersenne  43788  lighneallem2  43791  lighneallem4  43795  fppr2odd  43916  gbegt5  43946  gbowge7  43948  bgoldbtbndlem4  43993  bgoldbtbnd  43994  tgoldbach  44002  isomuspgrlem2b  44014  isomgrsym  44021  zrtermorngc  44292  zrtermoringc  44361  lcosslsp  44513  lindslinindsimp1  44532  snlindsntor  44546  m1modmmod  44601  eenglngeehlnmlem2  44745  itsclc0yqsol  44771  itschlc0xyqsol1  44773  itschlc0xyqsol  44774  setrec1lem4  44813  aacllem  44922