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  7276  fviunfun  7955  odi  8580  omass  8581  nndi  8625  nnmass  8626  omabslem  8652  domtrfil  9200  domnsymfi  9208  sdomdomtrfi  9209  domsdomtrfi  9210  php  9215  php3  9217  f1finf1o  9257  findcard3  9267  winainf  10772  divsubdir  12003  divdiv32  12018  ltdiv2  12196  peano2uz  13021  irrmul  13095  supxrunb1  13442  fzoshftral  13915  ltdifltdiv  13967  axdc4uzlem  14119  expdiv  14249  bcval5  14455  revpfxsfxrev  14910  rediv  15291  imdiv  15298  absdiflt  15478  absdifle  15479  iseraltlem3  15844  retancl  16303  tanneg  16309  difmod0  16450  lcmgcdeq  16780  prmdvdsexpb  16885  dvdsprmpweqnn  17056  mulgaddcomlem  19300  mulginvcom  19302  pmtrfb  19672  isdrng3lem2  20999  lspssp  21256  mdetunilem7  22926  m2detleiblem3  22937  m2detleiblem4  22938  pmatcollpw  23092  pmatcollpwscmat  23102  chpmatply1  23143  chfacfscmulgsum  23171  chfacfpmmulcl  23172  chfacfpmmul0  23173  chfacfpmmulgsum  23175  chfacfpmmulgsum2  23176  cayhamlem1  23177  cpmadurid  23178  cpmadugsumlemC  23186  cpmadugsumlemF  23187  cpmadugsumfi  23188  cpmidgsum2  23190  islp2  23456  fmfg  24261  fmufil  24271  flffbas  24307  lmflf  24317  uffcfflf  24351  blres  24743  ncvsge0  25467  caucfil  25597  cmetcusp1  25667  deg1mul3  26427  quotval  26606  ltonold  28640  cusgr3vnbpr  30010  clwwlkinwwlk  30624  nvsge0  31259  hvsubass  31639  hvsubdistr2  31645  hvsubcan  31669  his2sub  31687  chlub  32104  spanunsni  32174  homco1  32396  homulass  32397  cnlnadjlem2  32663  adjmul  32687  chirredlem2  32986  atmd2  32995  mdsymlem5  33002  climuzcnv  36415  pibt2  38320  f1ocan2fv  38641  isdrngo2  38872  atncvrN  40352  cvlatcvr1  40378  eluzrabdioph  43792  iocmbl  44199  rp-isfinite6  44503  ismnushort  45270  dvconstbi  45303  eelT11  45674  eelT12  45676  eelTT1  45677  eel0T1  45679  nn0digval  49681  dignn0flhalf  49699  sinhpcosh  50802  reseccl  50815  recsccl  50816  recotcl  50817  onetansqsecsq  50823