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

This theorem is referenced by:  3adant2l  1176  3adant2r  1177  syl3an2b  1402  syl3an2br  1405  fviunfun  7761  odi  8372  omass  8373  nndi  8416  nnmass  8417  omabslem  8440  winainf  10381  divsubdir  11599  divdiv32  11613  ltdiv2  11791  peano2uz  12570  irrmul  12643  supxrunb1  12982  fzoshftral  13432  ltdifltdiv  13482  axdc4uzlem  13631  expdiv  13762  bcval5  13960  ccats1val1OLD  14261  rediv  14770  imdiv  14777  absdiflt  14957  absdifle  14958  iseraltlem3  15323  retancl  15779  tanneg  15785  lcmgcdeq  16245  prmdvdsexpb  16349  dvdsprmpweqnn  16514  mulgaddcomlem  18641  mulginvcom  18643  pmtrfb  18988  lspssp  20165  mdetunilem7  21675  m2detleiblem3  21686  m2detleiblem4  21687  pmatcollpw  21838  pmatcollpwscmat  21848  chpmatply1  21889  chfacfscmulgsum  21917  chfacfpmmulcl  21918  chfacfpmmul0  21919  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadurid  21924  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmidgsum2  21936  islp2  22204  fmfg  23008  fmufil  23018  flffbas  23054  lmflf  23064  uffcfflf  23098  blres  23492  ncvsge0  24222  caucfil  24352  cmetcusp1  24422  deg1mul3  25185  quotval  25357  cusgr3vnbpr  27706  clwwlkinwwlk  28305  nvsge0  28927  hvsubass  29307  hvsubdistr2  29313  hvsubcan  29337  his2sub  29355  chlub  29772  spanunsni  29842  homco1  30064  homulass  30065  cnlnadjlem2  30331  adjmul  30355  chirredlem2  30654  atmd2  30663  mdsymlem5  30670  f1resrcmplf1dlem  32958  revpfxsfxrev  32977  climuzcnv  33529  pibt2  35515  f1ocan2fv  35812  isdrngo2  36043  atncvrN  37256  cvlatcvr1  37282  eluzrabdioph  40544  iocmbl  40960  rp-isfinite6  41023  ismnushort  41808  dvconstbi  41841  eelT11  42216  eelT12  42218  eelTT1  42219  eel0T1  42221  nn0digval  45834  dignn0flhalf  45852  sinhpcosh  46328  reseccl  46341  recsccl  46342  recotcl  46343  onetansqsecsq  46349