Theorem syl3an2 1180

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adant2l  1195  3adant2r  1196  syl3an2b  1429  syl3an2br  1432  fviunfun  7938  odi  8560  omass  8561  nndi  8605  nnmass  8606  omabslem  8632  domtrfil  9172  domnsymfi  9180  sdomdomtrfi  9181  domsdomtrfi  9182  php  9187  php3  9189  f1finf1o  9229  findcard3  9239  winainf  10675  divsubdir  11904  divdiv32  11919  ltdiv2  12097  peano2uz  12921  irrmul  12994  supxrunb1  13341  fzoshftral  13812  ltdifltdiv  13863  axdc4uzlem  14015  expdiv  14145  bcval5  14350  rediv  15178  imdiv  15185  absdiflt  15365  absdifle  15366  iseraltlem3  15731  retancl  16194  tanneg  16200  difmod0  16341  lcmgcdeq  16666  prmdvdsexpb  16771  dvdsprmpweqnn  16941  mulgaddcomlem  19159  mulginvcom  19161  pmtrfb  19531  lspssp  21083  mdetunilem7  22740  m2detleiblem3  22751  m2detleiblem4  22752  pmatcollpw  22903  pmatcollpwscmat  22913  chpmatply1  22954  chfacfscmulgsum  22982  chfacfpmmulcl  22983  chfacfpmmul0  22984  chfacfpmmulgsum  22986  chfacfpmmulgsum2  22987  cayhamlem1  22988  cpmadurid  22989  cpmadugsumlemC  22997  cpmadugsumlemF  22998  cpmadugsumfi  22999  cpmidgsum2  23001  islp2  23267  fmfg  24071  fmufil  24081  flffbas  24117  lmflf  24127  uffcfflf  24161  blres  24553  ncvsge0  25277  caucfil  25407  cmetcusp1  25477  deg1mul3  26238  quotval  26418  ltonold  28416  cusgr3vnbpr  29723  clwwlkinwwlk  30328  nvsge0  30953  hvsubass  31333  hvsubdistr2  31339  hvsubcan  31363  his2sub  31381  chlub  31798  spanunsni  31868  homco1  32090  homulass  32091  cnlnadjlem2  32357  adjmul  32381  chirredlem2  32680  atmd2  32689  mdsymlem5  32696  f1resrcmplf1dlem  35414  revpfxsfxrev  35502  climuzcnv  36058  pibt2  37946  f1ocan2fv  38261  isdrngo2  38492  atncvrN  39974  cvlatcvr1  40000  eluzrabdioph  43418  iocmbl  43825  rp-isfinite6  44129  ismnushort  44896  dvconstbi  44929  eelT11  45300  eelT12  45302  eelTT1  45303  eel0T1  45305  nn0digval  49258  dignn0flhalf  49276  sinhpcosh  50396  reseccl  50409  recsccl  50410  recotcl  50411  onetansqsecsq  50417