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 401  df-3an 1105

This theorem is used by:  3adant2l  1197  3adant2r  1198  syl3an2b  1431  syl3an2br  1434  fviunfun  7938  odi  8560  omass  8561  nndi  8605  nnmass  8606  omabslem  8632  domtrfil  9172  domnsymfi  9180  sdomdomtrfi  9181  domsdomtrfi  9182  php  9187  php3  9189  f1finf1o  9229  findcard3  9239  winainf  10683  divsubdir  11912  divdiv32  11927  ltdiv2  12105  peano2uz  12929  irrmul  13002  supxrunb1  13349  fzoshftral  13821  ltdifltdiv  13872  axdc4uzlem  14024  expdiv  14154  bcval5  14359  rediv  15187  imdiv  15194  absdiflt  15374  absdifle  15375  iseraltlem3  15740  retancl  16202  tanneg  16208  difmod0  16349  lcmgcdeq  16674  prmdvdsexpb  16779  dvdsprmpweqnn  16949  mulgaddcomlem  19167  mulginvcom  19169  pmtrfb  19539  isdrng3lem2  20861  lspssp  21118  mdetunilem7  22784  m2detleiblem3  22795  m2detleiblem4  22796  pmatcollpw  22947  pmatcollpwscmat  22957  chpmatply1  22998  chfacfscmulgsum  23026  chfacfpmmulcl  23027  chfacfpmmul0  23028  chfacfpmmulgsum  23030  chfacfpmmulgsum2  23031  cayhamlem1  23032  cpmadurid  23033  cpmadugsumlemC  23041  cpmadugsumlemF  23042  cpmadugsumfi  23043  cpmidgsum2  23045  islp2  23311  fmfg  24115  fmufil  24125  flffbas  24161  lmflf  24171  uffcfflf  24205  blres  24597  ncvsge0  25321  caucfil  25451  cmetcusp1  25521  deg1mul3  26282  quotval  26462  ltonold  28463  cusgr3vnbpr  29795  clwwlkinwwlk  30400  nvsge0  31025  hvsubass  31405  hvsubdistr2  31411  hvsubcan  31435  his2sub  31453  chlub  31870  spanunsni  31940  homco1  32162  homulass  32163  cnlnadjlem2  32429  adjmul  32453  chirredlem2  32752  atmd2  32761  mdsymlem5  32768  f1resrcmplf1dlem  35483  revpfxsfxrev  35615  climuzcnv  36171  pibt2  38091  f1ocan2fv  38406  isdrngo2  38637  atncvrN  40117  cvlatcvr1  40143  eluzrabdioph  43561  iocmbl  43968  rp-isfinite6  44272  ismnushort  45039  dvconstbi  45072  eelT11  45443  eelT12  45445  eelTT1  45446  eel0T1  45448  nn0digval  49408  dignn0flhalf  49426  sinhpcosh  50546  reseccl  50559  recsccl  50560  recotcl  50561  onetansqsecsq  50567