Theorem syl3an2 1165

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adant2l  1179  3adant2r  1180  syl3an2b  1406  syl3an2br  1409  fviunfun  7969  odi  8617  omass  8618  nndi  8661  nnmass  8662  omabslem  8688  domtrfil  9232  domnsymfi  9240  sdomdomtrfi  9241  domsdomtrfi  9242  php  9247  php3  9249  f1finf1o  9305  findcard3  9318  winainf  10734  divsubdir  11961  divdiv32  11975  ltdiv2  12154  peano2uz  12943  irrmul  13016  supxrunb1  13361  fzoshftral  13823  ltdifltdiv  13874  axdc4uzlem  14024  expdiv  14154  bcval5  14357  rediv  15170  imdiv  15177  absdiflt  15356  absdifle  15357  iseraltlem3  15720  retancl  16178  tanneg  16184  lcmgcdeq  16649  prmdvdsexpb  16753  dvdsprmpweqnn  16923  mulgaddcomlem  19115  mulginvcom  19117  pmtrfb  19483  lspssp  20986  mdetunilem7  22624  m2detleiblem3  22635  m2detleiblem4  22636  pmatcollpw  22787  pmatcollpwscmat  22797  chpmatply1  22838  chfacfscmulgsum  22866  chfacfpmmulcl  22867  chfacfpmmul0  22868  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmadurid  22873  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmidgsum2  22885  islp2  23153  fmfg  23957  fmufil  23967  flffbas  24003  lmflf  24013  uffcfflf  24047  blres  24441  ncvsge0  25187  caucfil  25317  cmetcusp1  25387  deg1mul3  26155  quotval  26334  sltonold  28283  cusgr3vnbpr  29453  clwwlkinwwlk  30059  nvsge0  30683  hvsubass  31063  hvsubdistr2  31069  hvsubcan  31093  his2sub  31111  chlub  31528  spanunsni  31598  homco1  31820  homulass  31821  cnlnadjlem2  32087  adjmul  32111  chirredlem2  32410  atmd2  32419  mdsymlem5  32426  f1resrcmplf1dlem  35100  revpfxsfxrev  35121  climuzcnv  35676  pibt2  37418  f1ocan2fv  37734  isdrngo2  37965  atncvrN  39316  cvlatcvr1  39342  eluzrabdioph  42817  iocmbl  43225  rp-isfinite6  43531  ismnushort  44320  dvconstbi  44353  eelT11  44727  eelT12  44729  eelTT1  44730  eel0T1  44732  nn0digval  48521  dignn0flhalf  48539  sinhpcosh  49259  reseccl  49272  recsccl  49273  recotcl  49274  onetansqsecsq  49280