Theorem syl3an2 1164

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 1153	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an2.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant2l  1178  3adant2r  1179  syl3an2b  1404  syl3an2br  1407  fviunfun  7985  odi  8635  omass  8636  nndi  8679  nnmass  8680  omabslem  8706  domtrfil  9258  domnsymfi  9266  sdomdomtrfi  9267  domsdomtrfi  9268  php  9273  php3  9275  f1finf1o  9333  findcard3  9346  winainf  10763  divsubdir  11988  divdiv32  12002  ltdiv2  12181  peano2uz  12966  irrmul  13039  supxrunb1  13381  fzoshftral  13834  ltdifltdiv  13885  axdc4uzlem  14034  expdiv  14164  bcval5  14367  rediv  15180  imdiv  15187  absdiflt  15366  absdifle  15367  iseraltlem3  15732  retancl  16190  tanneg  16196  lcmgcdeq  16659  prmdvdsexpb  16763  dvdsprmpweqnn  16932  mulgaddcomlem  19137  mulginvcom  19139  pmtrfb  19507  lspssp  21009  mdetunilem7  22645  m2detleiblem3  22656  m2detleiblem4  22657  pmatcollpw  22808  pmatcollpwscmat  22818  chpmatply1  22859  chfacfscmulgsum  22887  chfacfpmmulcl  22888  chfacfpmmul0  22889  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmadurid  22894  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmidgsum2  22906  islp2  23174  fmfg  23978  fmufil  23988  flffbas  24024  lmflf  24034  uffcfflf  24068  blres  24462  ncvsge0  25206  caucfil  25336  cmetcusp1  25406  deg1mul3  26175  quotval  26352  sltonold  28301  cusgr3vnbpr  29471  clwwlkinwwlk  30072  nvsge0  30696  hvsubass  31076  hvsubdistr2  31082  hvsubcan  31106  his2sub  31124  chlub  31541  spanunsni  31611  homco1  31833  homulass  31834  cnlnadjlem2  32100  adjmul  32124  chirredlem2  32423  atmd2  32432  mdsymlem5  32439  f1resrcmplf1dlem  35062  revpfxsfxrev  35083  climuzcnv  35639  pibt2  37383  f1ocan2fv  37687  isdrngo2  37918  atncvrN  39271  cvlatcvr1  39297  eluzrabdioph  42762  iocmbl  43174  rp-isfinite6  43480  ismnushort  44270  dvconstbi  44303  eelT11  44678  eelT12  44680  eelTT1  44681  eel0T1  44683  nn0digval  48334  dignn0flhalf  48352  sinhpcosh  48832  reseccl  48845  recsccl  48846  recotcl  48847  onetansqsecsq  48853