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  7877  odi  8494  omass  8495  nndi  8538  nnmass  8539  omabslem  8565  domtrfil  9101  domnsymfi  9109  sdomdomtrfi  9110  domsdomtrfi  9111  php  9116  php3  9118  f1finf1o  9157  findcard3  9167  winainf  10585  divsubdir  11815  divdiv32  11829  ltdiv2  12008  peano2uz  12799  irrmul  12872  supxrunb1  13218  fzoshftral  13687  ltdifltdiv  13738  axdc4uzlem  13890  expdiv  14020  bcval5  14225  rediv  15038  imdiv  15045  absdiflt  15225  absdifle  15226  iseraltlem3  15591  retancl  16051  tanneg  16057  difmod0  16198  lcmgcdeq  16523  prmdvdsexpb  16627  dvdsprmpweqnn  16797  mulgaddcomlem  19010  mulginvcom  19012  pmtrfb  19377  lspssp  20921  mdetunilem7  22533  m2detleiblem3  22544  m2detleiblem4  22545  pmatcollpw  22696  pmatcollpwscmat  22706  chpmatply1  22747  chfacfscmulgsum  22775  chfacfpmmulcl  22776  chfacfpmmul0  22777  chfacfpmmulgsum  22779  chfacfpmmulgsum2  22780  cayhamlem1  22781  cpmadurid  22782  cpmadugsumlemC  22790  cpmadugsumlemF  22791  cpmadugsumfi  22792  cpmidgsum2  22794  islp2  23060  fmfg  23864  fmufil  23874  flffbas  23910  lmflf  23920  uffcfflf  23954  blres  24346  ncvsge0  25080  caucfil  25210  cmetcusp1  25280  deg1mul3  26048  quotval  26227  sltonold  28198  cusgr3vnbpr  29414  clwwlkinwwlk  30020  nvsge0  30644  hvsubass  31024  hvsubdistr2  31030  hvsubcan  31054  his2sub  31072  chlub  31489  spanunsni  31559  homco1  31781  homulass  31782  cnlnadjlem2  32048  adjmul  32072  chirredlem2  32371  atmd2  32380  mdsymlem5  32387  f1resrcmplf1dlem  35098  revpfxsfxrev  35160  climuzcnv  35715  pibt2  37461  f1ocan2fv  37766  isdrngo2  37997  atncvrN  39413  cvlatcvr1  39439  eluzrabdioph  42898  iocmbl  43305  rp-isfinite6  43610  ismnushort  44393  dvconstbi  44426  eelT11  44798  eelT12  44800  eelTT1  44801  eel0T1  44803  nn0digval  48700  dignn0flhalf  48718  sinhpcosh  49840  reseccl  49853  recsccl  49854  recotcl  49855  onetansqsecsq  49861