Theorem syl3an2 1163

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 1152	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3adant2l  1177  3adant2r  1178  syl3an2b  1403  syl3an2br  1406  fviunfun  7787  odi  8410  omass  8411  nndi  8454  nnmass  8455  omabslem  8480  domtrfil  8978  domnsymfi  8986  sdomdomtrfi  8987  domsdomtrfi  8988  php  8993  php3  8995  winainf  10450  divsubdir  11669  divdiv32  11683  ltdiv2  11861  peano2uz  12641  irrmul  12714  supxrunb1  13053  fzoshftral  13504  ltdifltdiv  13554  axdc4uzlem  13703  expdiv  13834  bcval5  14032  ccats1val1OLD  14333  rediv  14842  imdiv  14849  absdiflt  15029  absdifle  15030  iseraltlem3  15395  retancl  15851  tanneg  15857  lcmgcdeq  16317  prmdvdsexpb  16421  dvdsprmpweqnn  16586  mulgaddcomlem  18726  mulginvcom  18728  pmtrfb  19073  lspssp  20250  mdetunilem7  21767  m2detleiblem3  21778  m2detleiblem4  21779  pmatcollpw  21930  pmatcollpwscmat  21940  chpmatply1  21981  chfacfscmulgsum  22009  chfacfpmmulcl  22010  chfacfpmmul0  22011  chfacfpmmulgsum  22013  chfacfpmmulgsum2  22014  cayhamlem1  22015  cpmadurid  22016  cpmadugsumlemC  22024  cpmadugsumlemF  22025  cpmadugsumfi  22026  cpmidgsum2  22028  islp2  22296  fmfg  23100  fmufil  23110  flffbas  23146  lmflf  23156  uffcfflf  23190  blres  23584  ncvsge0  24317  caucfil  24447  cmetcusp1  24517  deg1mul3  25280  quotval  25452  cusgr3vnbpr  27803  clwwlkinwwlk  28404  nvsge0  29026  hvsubass  29406  hvsubdistr2  29412  hvsubcan  29436  his2sub  29454  chlub  29871  spanunsni  29941  homco1  30163  homulass  30164  cnlnadjlem2  30430  adjmul  30454  chirredlem2  30753  atmd2  30762  mdsymlem5  30769  f1resrcmplf1dlem  33058  revpfxsfxrev  33077  climuzcnv  33629  pibt2  35588  f1ocan2fv  35885  isdrngo2  36116  atncvrN  37329  cvlatcvr1  37355  eluzrabdioph  40628  iocmbl  41044  rp-isfinite6  41125  ismnushort  41919  dvconstbi  41952  eelT11  42327  eelT12  42329  eelTT1  42330  eel0T1  42332  nn0digval  45946  dignn0flhalf  45964  sinhpcosh  46442  reseccl  46455  recsccl  46456  recotcl  46457  onetansqsecsq  46463