Theorem syl3an2 1164

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant2l  1179  3adant2r  1180  syl3an2b  1406  syl3an2br  1409  fviunfun  7903  odi  8520  omass  8521  nndi  8564  nnmass  8565  omabslem  8591  domtrfil  9133  domnsymfi  9141  sdomdomtrfi  9142  domsdomtrfi  9143  php  9148  php3  9150  f1finf1o  9192  findcard3  9205  winainf  10623  divsubdir  11852  divdiv32  11866  ltdiv2  12045  peano2uz  12836  irrmul  12909  supxrunb1  13255  fzoshftral  13721  ltdifltdiv  13772  axdc4uzlem  13924  expdiv  14054  bcval5  14259  rediv  15073  imdiv  15080  absdiflt  15260  absdifle  15261  iseraltlem3  15626  retancl  16086  tanneg  16092  difmod0  16233  lcmgcdeq  16558  prmdvdsexpb  16662  dvdsprmpweqnn  16832  mulgaddcomlem  19005  mulginvcom  19007  pmtrfb  19371  lspssp  20870  mdetunilem7  22481  m2detleiblem3  22492  m2detleiblem4  22493  pmatcollpw  22644  pmatcollpwscmat  22654  chpmatply1  22695  chfacfscmulgsum  22723  chfacfpmmulcl  22724  chfacfpmmul0  22725  chfacfpmmulgsum  22727  chfacfpmmulgsum2  22728  cayhamlem1  22729  cpmadurid  22730  cpmadugsumlemC  22738  cpmadugsumlemF  22739  cpmadugsumfi  22740  cpmidgsum2  22742  islp2  23008  fmfg  23812  fmufil  23822  flffbas  23858  lmflf  23868  uffcfflf  23902  blres  24295  ncvsge0  25029  caucfil  25159  cmetcusp1  25229  deg1mul3  25997  quotval  26176  sltonold  28138  cusgr3vnbpr  29339  clwwlkinwwlk  29942  nvsge0  30566  hvsubass  30946  hvsubdistr2  30952  hvsubcan  30976  his2sub  30994  chlub  31411  spanunsni  31481  homco1  31703  homulass  31704  cnlnadjlem2  31970  adjmul  31994  chirredlem2  32293  atmd2  32302  mdsymlem5  32309  f1resrcmplf1dlem  35049  revpfxsfxrev  35076  climuzcnv  35631  pibt2  37378  f1ocan2fv  37694  isdrngo2  37925  atncvrN  39281  cvlatcvr1  39307  eluzrabdioph  42767  iocmbl  43175  rp-isfinite6  43480  ismnushort  44263  dvconstbi  44296  eelT11  44669  eelT12  44671  eelTT1  44672  eel0T1  44674  nn0digval  48562  dignn0flhalf  48580  sinhpcosh  49702  reseccl  49715  recsccl  49716  recotcl  49717  onetansqsecsq  49723