Theorem syl3an2 1157

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

Syntax hints:   → wi 4   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3adant2l  1171  3adant2r  1172  syl3an2b  1397  syl3an2br  1400  fviunfun  7509  odi  8062  omass  8063  nndi  8106  nnmass  8107  omabslem  8130  winainf  9969  divsubdir  11188  divdiv32  11202  ltdiv2  11380  peano2uz  12154  irrmul  12227  supxrunb1  12566  fzoshftral  13008  ltdifltdiv  13058  axdc4uzlem  13205  expdiv  13334  bcval5  13532  ccats1val1  13828  rediv  14328  imdiv  14335  absdiflt  14515  absdifle  14516  iseraltlem3  14878  retancl  15332  tanneg  15338  lcmgcdeq  15789  prmdvdsexpb  15893  dvdsprmpweqnn  16054  mulgaddcomlem  18008  mulginvcom  18010  pmtrfb  18328  lspssp  19454  mdetunilem7  20915  m2detleiblem3  20926  m2detleiblem4  20927  pmatcollpw  21077  pmatcollpwscmat  21087  chpmatply1  21128  chfacfscmulgsum  21156  chfacfpmmulcl  21157  chfacfpmmul0  21158  chfacfpmmulgsum  21160  chfacfpmmulgsum2  21161  cayhamlem1  21162  cpmadurid  21163  cpmadugsumlemC  21171  cpmadugsumlemF  21172  cpmadugsumfi  21173  cpmidgsum2  21175  islp2  21441  fmfg  22245  fmufil  22255  flffbas  22291  lmflf  22301  uffcfflf  22335  blres  22728  ncvsge0  23444  caucfil  23573  cmetcusp1  23643  deg1mul3  24396  quotval  24568  cusgr3vnbpr  26905  clwwlkinwwlk  27504  nvsge0  28128  hvsubass  28508  hvsubdistr2  28514  hvsubcan  28538  his2sub  28556  chlub  28973  spanunsni  29043  homco1  29265  homulass  29266  cnlnadjlem2  29532  adjmul  29556  chirredlem2  29855  atmd2  29864  mdsymlem5  29871  f1resrcmplf1dlem  31969  revpfxsfxrev  31972  climuzcnv  32524  pibt2  34250  f1ocan2fv  34555  isdrngo2  34789  atncvrN  36003  cvlatcvr1  36029  eluzrabdioph  38909  iocmbl  39325  rp-isfinite6  39390  dvconstbi  40225  eelT11  40601  eelT12  40603  eelTT1  40604  eel0T1  40606  nn0digval  44163  dignn0flhalf  44181  sinhpcosh  44341  reseccl  44354  recsccl  44355  recotcl  44356  onetansqsecsq  44362