Theorem syl3an2 1160

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3adant2l  1174  3adant2r  1175  syl3an2b  1400  syl3an2br  1403  fviunfun  7640  odi  8199  omass  8200  nndi  8243  nnmass  8244  omabslem  8267  winainf  10110  divsubdir  11328  divdiv32  11342  ltdiv2  11520  peano2uz  12295  irrmul  12367  supxrunb1  12706  fzoshftral  13148  ltdifltdiv  13198  axdc4uzlem  13345  expdiv  13474  bcval5  13672  ccats1val1OLD  13976  rediv  14484  imdiv  14491  absdiflt  14671  absdifle  14672  iseraltlem3  15034  retancl  15489  tanneg  15495  lcmgcdeq  15950  prmdvdsexpb  16054  dvdsprmpweqnn  16215  mulgaddcomlem  18244  mulginvcom  18246  pmtrfb  18587  lspssp  19754  mdetunilem7  21221  m2detleiblem3  21232  m2detleiblem4  21233  pmatcollpw  21383  pmatcollpwscmat  21393  chpmatply1  21434  chfacfscmulgsum  21462  chfacfpmmulcl  21463  chfacfpmmul0  21464  chfacfpmmulgsum  21466  chfacfpmmulgsum2  21467  cayhamlem1  21468  cpmadurid  21469  cpmadugsumlemC  21477  cpmadugsumlemF  21478  cpmadugsumfi  21479  cpmidgsum2  21481  islp2  21747  fmfg  22551  fmufil  22561  flffbas  22597  lmflf  22607  uffcfflf  22641  blres  23035  ncvsge0  23751  caucfil  23880  cmetcusp1  23950  deg1mul3  24703  quotval  24875  cusgr3vnbpr  27212  clwwlkinwwlk  27812  nvsge0  28435  hvsubass  28815  hvsubdistr2  28821  hvsubcan  28845  his2sub  28863  chlub  29280  spanunsni  29350  homco1  29572  homulass  29573  cnlnadjlem2  29839  adjmul  29863  chirredlem2  30162  atmd2  30171  mdsymlem5  30178  f1resrcmplf1dlem  32354  revpfxsfxrev  32357  climuzcnv  32909  pibt2  34692  f1ocan2fv  34996  isdrngo2  35230  atncvrN  36445  cvlatcvr1  36471  eluzrabdioph  39396  iocmbl  39812  rp-isfinite6  39877  dvconstbi  40659  eelT11  41034  eelT12  41036  eelTT1  41037  eel0T1  41039  nn0digval  44654  dignn0flhalf  44672  sinhpcosh  44833  reseccl  44846  recsccl  44847  recotcl  44848  onetansqsecsq  44854