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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant2l  1177  3adant2r  1178  syl3an2b  1403  syl3an2br  1406  fviunfun  7967  odi  8615  omass  8616  nndi  8659  nnmass  8660  omabslem  8686  domtrfil  9229  domnsymfi  9237  sdomdomtrfi  9238  domsdomtrfi  9239  php  9244  php3  9246  f1finf1o  9302  findcard3  9315  winainf  10731  divsubdir  11958  divdiv32  11972  ltdiv2  12151  peano2uz  12940  irrmul  13013  supxrunb1  13357  fzoshftral  13819  ltdifltdiv  13870  axdc4uzlem  14020  expdiv  14150  bcval5  14353  rediv  15166  imdiv  15173  absdiflt  15352  absdifle  15353  iseraltlem3  15716  retancl  16174  tanneg  16180  lcmgcdeq  16645  prmdvdsexpb  16749  dvdsprmpweqnn  16918  mulgaddcomlem  19127  mulginvcom  19129  pmtrfb  19497  lspssp  21003  mdetunilem7  22639  m2detleiblem3  22650  m2detleiblem4  22651  pmatcollpw  22802  pmatcollpwscmat  22812  chpmatply1  22853  chfacfscmulgsum  22881  chfacfpmmulcl  22882  chfacfpmmul0  22883  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadurid  22888  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cpmadugsumfi  22898  cpmidgsum2  22900  islp2  23168  fmfg  23972  fmufil  23982  flffbas  24018  lmflf  24028  uffcfflf  24062  blres  24456  ncvsge0  25200  caucfil  25330  cmetcusp1  25400  deg1mul3  26169  quotval  26348  sltonold  28297  cusgr3vnbpr  29467  clwwlkinwwlk  30068  nvsge0  30692  hvsubass  31072  hvsubdistr2  31078  hvsubcan  31102  his2sub  31120  chlub  31537  spanunsni  31607  homco1  31829  homulass  31830  cnlnadjlem2  32096  adjmul  32120  chirredlem2  32419  atmd2  32428  mdsymlem5  32435  f1resrcmplf1dlem  35078  revpfxsfxrev  35099  climuzcnv  35655  pibt2  37399  f1ocan2fv  37713  isdrngo2  37944  atncvrN  39296  cvlatcvr1  39322  eluzrabdioph  42793  iocmbl  43201  rp-isfinite6  43507  ismnushort  44296  dvconstbi  44329  eelT11  44704  eelT12  44706  eelTT1  44707  eel0T1  44709  nn0digval  48449  dignn0flhalf  48467  sinhpcosh  48970  reseccl  48983  recsccl  48984  recotcl  48985  onetansqsecsq  48991