Theorem syl3an2 1160

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant2l  1174  3adant2r  1175  syl3an2b  1400  syl3an2br  1403  fviunfun  7646  odi  8205  omass  8206  nndi  8249  nnmass  8250  omabslem  8273  winainf  10116  divsubdir  11334  divdiv32  11348  ltdiv2  11526  peano2uz  12302  irrmul  12374  supxrunb1  12713  fzoshftral  13155  ltdifltdiv  13205  axdc4uzlem  13352  expdiv  13481  bcval5  13679  ccats1val1OLD  13982  rediv  14490  imdiv  14497  absdiflt  14677  absdifle  14678  iseraltlem3  15040  retancl  15495  tanneg  15501  lcmgcdeq  15956  prmdvdsexpb  16060  dvdsprmpweqnn  16221  mulgaddcomlem  18250  mulginvcom  18252  pmtrfb  18593  lspssp  19760  mdetunilem7  21227  m2detleiblem3  21238  m2detleiblem4  21239  pmatcollpw  21389  pmatcollpwscmat  21399  chpmatply1  21440  chfacfscmulgsum  21468  chfacfpmmulcl  21469  chfacfpmmul0  21470  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadurid  21475  cpmadugsumlemC  21483  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmidgsum2  21487  islp2  21753  fmfg  22557  fmufil  22567  flffbas  22603  lmflf  22613  uffcfflf  22647  blres  23041  ncvsge0  23757  caucfil  23886  cmetcusp1  23956  deg1mul3  24709  quotval  24881  cusgr3vnbpr  27218  clwwlkinwwlk  27818  nvsge0  28441  hvsubass  28821  hvsubdistr2  28827  hvsubcan  28851  his2sub  28869  chlub  29286  spanunsni  29356  homco1  29578  homulass  29579  cnlnadjlem2  29845  adjmul  29869  chirredlem2  30168  atmd2  30177  mdsymlem5  30184  f1resrcmplf1dlem  32359  revpfxsfxrev  32362  climuzcnv  32914  pibt2  34701  f1ocan2fv  35017  isdrngo2  35251  atncvrN  36466  cvlatcvr1  36492  eluzrabdioph  39423  iocmbl  39839  rp-isfinite6  39904  dvconstbi  40686  eelT11  41061  eelT12  41063  eelTT1  41064  eel0T1  41066  nn0digval  44680  dignn0flhalf  44698  sinhpcosh  44859  reseccl  44872  recsccl  44873  recotcl  44874  onetansqsecsq  44880