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  7889  odi  8506  omass  8507  nndi  8551  nnmass  8552  omabslem  8578  domtrfil  9116  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  php3  9133  f1finf1o  9173  findcard3  9183  winainf  10605  divsubdir  11835  divdiv32  11849  ltdiv2  12028  peano2uz  12814  irrmul  12887  supxrunb1  13234  fzoshftral  13703  ltdifltdiv  13754  axdc4uzlem  13906  expdiv  14036  bcval5  14241  rediv  15054  imdiv  15061  absdiflt  15241  absdifle  15242  iseraltlem3  15607  retancl  16067  tanneg  16073  difmod0  16214  lcmgcdeq  16539  prmdvdsexpb  16643  dvdsprmpweqnn  16813  mulgaddcomlem  19027  mulginvcom  19029  pmtrfb  19394  lspssp  20939  mdetunilem7  22562  m2detleiblem3  22573  m2detleiblem4  22574  pmatcollpw  22725  pmatcollpwscmat  22735  chpmatply1  22776  chfacfscmulgsum  22804  chfacfpmmulcl  22805  chfacfpmmul0  22806  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadurid  22811  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cpmadugsumfi  22821  cpmidgsum2  22823  islp2  23089  fmfg  23893  fmufil  23903  flffbas  23939  lmflf  23949  uffcfflf  23983  blres  24375  ncvsge0  25109  caucfil  25239  cmetcusp1  25309  deg1mul3  26077  quotval  26256  ltonold  28257  cusgr3vnbpr  29509  clwwlkinwwlk  30115  nvsge0  30739  hvsubass  31119  hvsubdistr2  31125  hvsubcan  31149  his2sub  31167  chlub  31584  spanunsni  31654  homco1  31876  homulass  31877  cnlnadjlem2  32143  adjmul  32167  chirredlem2  32466  atmd2  32475  mdsymlem5  32482  f1resrcmplf1dlem  35242  revpfxsfxrev  35310  climuzcnv  35865  pibt2  37622  f1ocan2fv  37928  isdrngo2  38159  atncvrN  39575  cvlatcvr1  39601  eluzrabdioph  43048  iocmbl  43455  rp-isfinite6  43759  ismnushort  44542  dvconstbi  44575  eelT11  44947  eelT12  44949  eelTT1  44950  eel0T1  44952  nn0digval  48846  dignn0flhalf  48864  sinhpcosh  49985  reseccl  49998  recsccl  49999  recotcl  50000  onetansqsecsq  50006