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  7781  odi  8395  omass  8396  nndi  8439  nnmass  8440  omabslem  8463  domtrfil  8960  domnsymfi  8968  sdomdomtrfi  8969  domsdomtrfi  8970  php  8974  php3  8976  winainf  10451  divsubdir  11669  divdiv32  11683  ltdiv2  11861  peano2uz  12640  irrmul  12713  supxrunb1  13052  fzoshftral  13502  ltdifltdiv  13552  axdc4uzlem  13701  expdiv  13832  bcval5  14030  ccats1val1OLD  14331  rediv  14840  imdiv  14847  absdiflt  15027  absdifle  15028  iseraltlem3  15393  retancl  15849  tanneg  15855  lcmgcdeq  16315  prmdvdsexpb  16419  dvdsprmpweqnn  16584  mulgaddcomlem  18724  mulginvcom  18726  pmtrfb  19071  lspssp  20248  mdetunilem7  21765  m2detleiblem3  21776  m2detleiblem4  21777  pmatcollpw  21928  pmatcollpwscmat  21938  chpmatply1  21979  chfacfscmulgsum  22007  chfacfpmmulcl  22008  chfacfpmmul0  22009  chfacfpmmulgsum  22011  chfacfpmmulgsum2  22012  cayhamlem1  22013  cpmadurid  22014  cpmadugsumlemC  22022  cpmadugsumlemF  22023  cpmadugsumfi  22024  cpmidgsum2  22026  islp2  22294  fmfg  23098  fmufil  23108  flffbas  23144  lmflf  23154  uffcfflf  23188  blres  23582  ncvsge0  24315  caucfil  24445  cmetcusp1  24515  deg1mul3  25278  quotval  25450  cusgr3vnbpr  27801  clwwlkinwwlk  28400  nvsge0  29022  hvsubass  29402  hvsubdistr2  29408  hvsubcan  29432  his2sub  29450  chlub  29867  spanunsni  29937  homco1  30159  homulass  30160  cnlnadjlem2  30426  adjmul  30450  chirredlem2  30749  atmd2  30758  mdsymlem5  30765  f1resrcmplf1dlem  33054  revpfxsfxrev  33073  climuzcnv  33625  pibt2  35584  f1ocan2fv  35881  isdrngo2  36112  atncvrN  37325  cvlatcvr1  37351  eluzrabdioph  40625  iocmbl  41041  rp-isfinite6  41104  ismnushort  41889  dvconstbi  41922  eelT11  42297  eelT12  42299  eelTT1  42300  eel0T1  42302  nn0digval  45915  dignn0flhalf  45933  sinhpcosh  46411  reseccl  46424  recsccl  46425  recotcl  46426  onetansqsecsq  46432