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  7271  fviunfun  7942  odi  8566  omass  8567  nndi  8611  nnmass  8612  omabslem  8638  domtrfil  9186  domnsymfi  9194  sdomdomtrfi  9195  domsdomtrfi  9196  php  9201  php3  9203  f1finf1o  9243  findcard3  9253  winainf  10703  divsubdir  11932  divdiv32  11947  ltdiv2  12125  peano2uz  12950  irrmul  13024  supxrunb1  13371  fzoshftral  13843  ltdifltdiv  13895  axdc4uzlem  14047  expdiv  14177  bcval5  14382  revpfxsfxrev  14837  rediv  15218  imdiv  15225  absdiflt  15405  absdifle  15406  iseraltlem3  15771  retancl  16230  tanneg  16236  difmod0  16377  lcmgcdeq  16702  prmdvdsexpb  16807  dvdsprmpweqnn  16977  mulgaddcomlem  19220  mulginvcom  19222  pmtrfb  19592  isdrng3lem2  20915  lspssp  21172  mdetunilem7  22840  m2detleiblem3  22851  m2detleiblem4  22852  pmatcollpw  23006  pmatcollpwscmat  23016  chpmatply1  23057  chfacfscmulgsum  23085  chfacfpmmulcl  23086  chfacfpmmul0  23087  chfacfpmmulgsum  23089  chfacfpmmulgsum2  23090  cayhamlem1  23091  cpmadurid  23092  cpmadugsumlemC  23100  cpmadugsumlemF  23101  cpmadugsumfi  23102  cpmidgsum2  23104  islp2  23370  fmfg  24175  fmufil  24185  flffbas  24221  lmflf  24231  uffcfflf  24265  blres  24657  ncvsge0  25381  caucfil  25511  cmetcusp1  25581  deg1mul3  26341  quotval  26522  ltonold  28526  cusgr3vnbpr  29896  clwwlkinwwlk  30510  nvsge0  31145  hvsubass  31525  hvsubdistr2  31531  hvsubcan  31555  his2sub  31573  chlub  31990  spanunsni  32060  homco1  32282  homulass  32283  cnlnadjlem2  32549  adjmul  32573  chirredlem2  32872  atmd2  32881  mdsymlem5  32888  climuzcnv  36250  pibt2  38171  f1ocan2fv  38477  isdrngo2  38708  atncvrN  40188  cvlatcvr1  40214  eluzrabdioph  43647  iocmbl  44054  rp-isfinite6  44358  ismnushort  45125  dvconstbi  45158  eelT11  45529  eelT12  45531  eelTT1  45532  eel0T1  45534  nn0digval  49530  dignn0flhalf  49548  sinhpcosh  50666  reseccl  50679  recsccl  50680  recotcl  50681  onetansqsecsq  50687