Theorem syl3an2 1176

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3adant2l  1191  3adant2r  1192  syl3an2b  1422  syl3an2br  1425  fviunfun  7920  odi  8541  omass  8542  nndi  8586  nnmass  8587  omabslem  8613  domtrfil  9153  domnsymfi  9161  sdomdomtrfi  9162  domsdomtrfi  9163  php  9168  php3  9170  f1finf1o  9210  findcard3  9220  winainf  10645  divsubdir  11877  divdiv32  11892  ltdiv2  12071  peano2uz  12895  irrmul  12968  supxrunb1  13315  fzoshftral  13786  ltdifltdiv  13837  axdc4uzlem  13989  expdiv  14119  bcval5  14324  rediv  15148  imdiv  15155  absdiflt  15335  absdifle  15336  iseraltlem3  15701  retancl  16164  tanneg  16170  difmod0  16311  lcmgcdeq  16636  prmdvdsexpb  16741  dvdsprmpweqnn  16911  mulgaddcomlem  19129  mulginvcom  19131  pmtrfb  19495  lspssp  21042  mdetunilem7  22665  m2detleiblem3  22676  m2detleiblem4  22677  pmatcollpw  22828  pmatcollpwscmat  22838  chpmatply1  22879  chfacfscmulgsum  22907  chfacfpmmulcl  22908  chfacfpmmul0  22909  chfacfpmmulgsum  22911  chfacfpmmulgsum2  22912  cayhamlem1  22913  cpmadurid  22914  cpmadugsumlemC  22922  cpmadugsumlemF  22923  cpmadugsumfi  22924  cpmidgsum2  22926  islp2  23192  fmfg  23996  fmufil  24006  flffbas  24042  lmflf  24052  uffcfflf  24086  blres  24478  ncvsge0  25202  caucfil  25332  cmetcusp1  25402  deg1mul3  26163  quotval  26343  ltonold  28341  cusgr3vnbpr  29593  clwwlkinwwlk  30198  nvsge0  30823  hvsubass  31203  hvsubdistr2  31209  hvsubcan  31233  his2sub  31251  chlub  31668  spanunsni  31738  homco1  31960  homulass  31961  cnlnadjlem2  32227  adjmul  32251  chirredlem2  32550  atmd2  32559  mdsymlem5  32566  f1resrcmplf1dlem  35340  revpfxsfxrev  35426  climuzcnv  35981  pibt2  37871  f1ocan2fv  38186  isdrngo2  38417  atncvrN  39899  cvlatcvr1  39925  eluzrabdioph  43343  iocmbl  43750  rp-isfinite6  44054  ismnushort  44837  dvconstbi  44870  eelT11  45242  eelT12  45244  eelTT1  45245  eel0T1  45247  nn0digval  49182  dignn0flhalf  49200  sinhpcosh  50321  reseccl  50334  recsccl  50335  recotcl  50336  onetansqsecsq  50342