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  7948  odi  8599  omass  8600  nndi  8643  nnmass  8644  omabslem  8670  domtrfil  9219  domnsymfi  9227  sdomdomtrfi  9228  domsdomtrfi  9229  php  9234  php3  9236  f1finf1o  9295  findcard3  9309  winainf  10717  divsubdir  11938  divdiv32  11952  ltdiv2  12130  peano2uz  12915  irrmul  12988  supxrunb1  13330  fzoshftral  13781  ltdifltdiv  13831  axdc4uzlem  13980  expdiv  14110  bcval5  14309  rediv  15110  imdiv  15117  absdiflt  15296  absdifle  15297  iseraltlem3  15662  retancl  16118  tanneg  16124  lcmgcdeq  16582  prmdvdsexpb  16686  dvdsprmpweqnn  16853  mulgaddcomlem  19051  mulginvcom  19053  pmtrfb  19419  lspssp  20871  mdetunilem7  22519  m2detleiblem3  22530  m2detleiblem4  22531  pmatcollpw  22682  pmatcollpwscmat  22692  chpmatply1  22733  chfacfscmulgsum  22761  chfacfpmmulcl  22762  chfacfpmmul0  22763  chfacfpmmulgsum  22765  chfacfpmmulgsum2  22766  cayhamlem1  22767  cpmadurid  22768  cpmadugsumlemC  22776  cpmadugsumlemF  22777  cpmadugsumfi  22778  cpmidgsum2  22780  islp2  23048  fmfg  23852  fmufil  23862  flffbas  23898  lmflf  23908  uffcfflf  23942  blres  24336  ncvsge0  25080  caucfil  25210  cmetcusp1  25280  deg1mul3  26050  quotval  26226  sltonold  28152  cusgr3vnbpr  29248  clwwlkinwwlk  29849  nvsge0  30473  hvsubass  30853  hvsubdistr2  30859  hvsubcan  30883  his2sub  30901  chlub  31318  spanunsni  31388  homco1  31610  homulass  31611  cnlnadjlem2  31877  adjmul  31901  chirredlem2  32200  atmd2  32209  mdsymlem5  32216  f1resrcmplf1dlem  34709  revpfxsfxrev  34725  climuzcnv  35275  pibt2  36896  f1ocan2fv  37200  isdrngo2  37431  atncvrN  38787  cvlatcvr1  38813  eluzrabdioph  42226  iocmbl  42641  rp-isfinite6  42948  ismnushort  43738  dvconstbi  43771  eelT11  44146  eelT12  44148  eelTT1  44149  eel0T1  44151  nn0digval  47673  dignn0flhalf  47691  sinhpcosh  48171  reseccl  48184  recsccl  48185  recotcl  48186  onetansqsecsq  48192