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  7941  odi  8589  omass  8590  nndi  8633  nnmass  8634  omabslem  8660  domtrfil  9204  domnsymfi  9212  sdomdomtrfi  9213  domsdomtrfi  9214  php  9219  php3  9221  f1finf1o  9275  findcard3  9288  winainf  10706  divsubdir  11933  divdiv32  11947  ltdiv2  12126  peano2uz  12915  irrmul  12988  supxrunb1  13333  fzoshftral  13798  ltdifltdiv  13849  axdc4uzlem  13999  expdiv  14129  bcval5  14334  rediv  15148  imdiv  15155  absdiflt  15334  absdifle  15335  iseraltlem3  15698  retancl  16158  tanneg  16164  lcmgcdeq  16629  prmdvdsexpb  16733  dvdsprmpweqnn  16903  mulgaddcomlem  19078  mulginvcom  19080  pmtrfb  19444  lspssp  20943  mdetunilem7  22554  m2detleiblem3  22565  m2detleiblem4  22566  pmatcollpw  22717  pmatcollpwscmat  22727  chpmatply1  22768  chfacfscmulgsum  22796  chfacfpmmulcl  22797  chfacfpmmul0  22798  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadurid  22803  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cpmadugsumfi  22813  cpmidgsum2  22815  islp2  23081  fmfg  23885  fmufil  23895  flffbas  23931  lmflf  23941  uffcfflf  23975  blres  24368  ncvsge0  25103  caucfil  25233  cmetcusp1  25303  deg1mul3  26071  quotval  26250  sltonold  28200  cusgr3vnbpr  29361  clwwlkinwwlk  29967  nvsge0  30591  hvsubass  30971  hvsubdistr2  30977  hvsubcan  31001  his2sub  31019  chlub  31436  spanunsni  31506  homco1  31728  homulass  31729  cnlnadjlem2  31995  adjmul  32019  chirredlem2  32318  atmd2  32327  mdsymlem5  32334  f1resrcmplf1dlem  35063  revpfxsfxrev  35084  climuzcnv  35639  pibt2  37381  f1ocan2fv  37697  isdrngo2  37928  atncvrN  39279  cvlatcvr1  39305  eluzrabdioph  42776  iocmbl  43184  rp-isfinite6  43489  ismnushort  44273  dvconstbi  44306  eelT11  44679  eelT12  44681  eelTT1  44682  eel0T1  44684  nn0digval  48528  dignn0flhalf  48546  sinhpcosh  49552  reseccl  49565  recsccl  49566  recotcl  49567  onetansqsecsq  49573