Theorem syl3an2 1182

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant2l  1197  3adant2r  1198  syl3an2b  1432  syl3an2br  1435  f1resrcmplf1dlem  7309  fviunfun  7991  odi  8625  omass  8626  nndi  8670  nnmass  8671  omabslem  8697  domtrfil  9245  domnsymfi  9253  sdomdomtrfi  9254  domsdomtrfi  9255  php  9260  php3  9262  f1finf1o  9302  findcard3  9312  ac6  10597  winainf  10818  divsubdir  12050  divdiv32  12065  ltdiv2  12243  peano2uz  13068  irrmul  13142  supxrunb1  13489  fzoshftral  13962  ltdifltdiv  14014  axdc4uzlem  14166  expdiv  14296  bcval5  14503  revpfxsfxrev  14959  rediv  15341  imdiv  15348  absdiflt  15528  absdifle  15529  iseraltlem3  15895  retancl  16354  tanneg  16360  difmod0  16501  lcmgcdeq  16831  prmdvdsexpb  16936  dvdsprmpweqnn  17107  mulgaddcomlem  19357  mulginvcom  19359  pmtrfb  19730  isdrng3lem2  21057  lspssp  21314  mdetunilem7  22988  m2detleiblem3  22999  m2detleiblem4  23000  pmatcollpw  23154  pmatcollpwscmat  23164  chpmatply1  23205  chfacfscmulgsum  23233  chfacfpmmulcl  23234  chfacfpmmul0  23235  chfacfpmmulgsum  23237  chfacfpmmulgsum2  23238  cayhamlem1  23239  cpmadurid  23240  cpmadugsumlemC  23248  cpmadugsumlemF  23249  cpmadugsumfi  23250  cpmidgsum2  23252  islp2  23518  fmfg  24323  fmufil  24333  flffbas  24369  lmflf  24379  uffcfflf  24413  blres  24805  ncvsge0  25529  caucfil  25659  cmetcusp1  25729  deg1mul3  26489  quotval  26668  ltonold  28704  cusgr3vnbpr  30074  clwwlkinwwlk  30688  nvsge0  31323  hvsubass  31703  hvsubdistr2  31709  hvsubcan  31733  his2sub  31751  chlub  32168  spanunsni  32238  homco1  32460  homulass  32461  cnlnadjlem2  32727  adjmul  32751  chirredlem2  33050  atmd2  33059  mdsymlem5  33066  climuzcnv  36644  pibt2  38608  f1ocan2fv  38929  isdrngo2  39158  atncvrN  40638  cvlatcvr1  40664  eluzrabdioph  44079  iocmbl  44476  rp-isfinite6  44780  ismnushort  45546  dvconstbi  45579  eelT11  45949  eelT12  45951  eelTT1  45952  eel0T1  45954  nn0digval  50043  dignn0flhalf  50061  sinhpcosh  51238  reseccl  51274  recsccl  51275  recotcl  51276  onetansqsecsq  51282