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  1431  syl3an2br  1434  f1resrcmplf1dlem  7279  fviunfun  7958  odi  8591  omass  8592  nndi  8636  nnmass  8637  omabslem  8663  domtrfil  9211  domnsymfi  9219  sdomdomtrfi  9220  domsdomtrfi  9221  php  9226  php3  9228  f1finf1o  9268  findcard3  9278  ac6  10562  winainf  10783  divsubdir  12014  divdiv32  12029  ltdiv2  12207  peano2uz  13032  irrmul  13106  supxrunb1  13453  fzoshftral  13926  ltdifltdiv  13978  axdc4uzlem  14130  expdiv  14260  bcval5  14466  revpfxsfxrev  14922  rediv  15304  imdiv  15311  absdiflt  15491  absdifle  15492  iseraltlem3  15857  retancl  16316  tanneg  16322  difmod0  16463  lcmgcdeq  16793  prmdvdsexpb  16898  dvdsprmpweqnn  17069  mulgaddcomlem  19313  mulginvcom  19315  pmtrfb  19685  isdrng3lem2  21012  lspssp  21269  mdetunilem7  22939  m2detleiblem3  22950  m2detleiblem4  22951  pmatcollpw  23105  pmatcollpwscmat  23115  chpmatply1  23156  chfacfscmulgsum  23184  chfacfpmmulcl  23185  chfacfpmmul0  23186  chfacfpmmulgsum  23188  chfacfpmmulgsum2  23189  cayhamlem1  23190  cpmadurid  23191  cpmadugsumlemC  23199  cpmadugsumlemF  23200  cpmadugsumfi  23201  cpmidgsum2  23203  islp2  23469  fmfg  24274  fmufil  24284  flffbas  24320  lmflf  24330  uffcfflf  24364  blres  24756  ncvsge0  25480  caucfil  25610  cmetcusp1  25680  deg1mul3  26440  quotval  26619  ltonold  28653  cusgr3vnbpr  30023  clwwlkinwwlk  30637  nvsge0  31272  hvsubass  31652  hvsubdistr2  31658  hvsubcan  31682  his2sub  31700  chlub  32117  spanunsni  32187  homco1  32409  homulass  32410  cnlnadjlem2  32676  adjmul  32700  chirredlem2  32999  atmd2  33008  mdsymlem5  33015  climuzcnv  36523  pibt2  38434  f1ocan2fv  38755  isdrngo2  38986  atncvrN  40466  cvlatcvr1  40492  eluzrabdioph  43907  iocmbl  44309  rp-isfinite6  44613  ismnushort  45379  dvconstbi  45412  eelT11  45783  eelT12  45785  eelTT1  45786  eel0T1  45788  nn0digval  49806  dignn0flhalf  49824  sinhpcosh  51002  reseccl  51015  recsccl  51016  recotcl  51017  onetansqsecsq  51023