Theorem syl3an2 1162

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

Ref	Expression
syl3an2.1	⊢ (𝜑 → 𝜒)
syl3an2.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an2	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	3anim2i 1151	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an2.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087

This theorem is referenced by:  3adant2l  1176  3adant2r  1177  syl3an2b  1402  syl3an2br  1405  fviunfun  7933  odi  8581  omass  8582  nndi  8625  nnmass  8626  omabslem  8651  domtrfil  9197  domnsymfi  9205  sdomdomtrfi  9206  domsdomtrfi  9207  php  9212  php3  9214  f1finf1o  9273  findcard3  9287  winainf  10691  divsubdir  11912  divdiv32  11926  ltdiv2  12104  peano2uz  12889  irrmul  12962  supxrunb1  13302  fzoshftral  13753  ltdifltdiv  13803  axdc4uzlem  13952  expdiv  14083  bcval5  14282  rediv  15082  imdiv  15089  absdiflt  15268  absdifle  15269  iseraltlem3  15634  retancl  16089  tanneg  16095  lcmgcdeq  16553  prmdvdsexpb  16657  dvdsprmpweqnn  16822  mulgaddcomlem  19013  mulginvcom  19015  pmtrfb  19374  lspssp  20743  mdetunilem7  22340  m2detleiblem3  22351  m2detleiblem4  22352  pmatcollpw  22503  pmatcollpwscmat  22513  chpmatply1  22554  chfacfscmulgsum  22582  chfacfpmmulcl  22583  chfacfpmmul0  22584  chfacfpmmulgsum  22586  chfacfpmmulgsum2  22587  cayhamlem1  22588  cpmadurid  22589  cpmadugsumlemC  22597  cpmadugsumlemF  22598  cpmadugsumfi  22599  cpmidgsum2  22601  islp2  22869  fmfg  23673  fmufil  23683  flffbas  23719  lmflf  23729  uffcfflf  23763  blres  24157  ncvsge0  24901  caucfil  25031  cmetcusp1  25101  deg1mul3  25868  quotval  26041  sltonold  27926  cusgr3vnbpr  28960  clwwlkinwwlk  29560  nvsge0  30184  hvsubass  30564  hvsubdistr2  30570  hvsubcan  30594  his2sub  30612  chlub  31029  spanunsni  31099  homco1  31321  homulass  31322  cnlnadjlem2  31588  adjmul  31612  chirredlem2  31911  atmd2  31920  mdsymlem5  31927  f1resrcmplf1dlem  34387  revpfxsfxrev  34404  climuzcnv  34954  pibt2  36601  f1ocan2fv  36898  isdrngo2  37129  atncvrN  38488  cvlatcvr1  38514  eluzrabdioph  41846  iocmbl  42264  rp-isfinite6  42571  ismnushort  43362  dvconstbi  43395  eelT11  43770  eelT12  43772  eelTT1  43773  eel0T1  43775  nn0digval  47373  dignn0flhalf  47391  sinhpcosh  47872  reseccl  47885  recsccl  47886  recotcl  47887  onetansqsecsq  47893