Theorem syl3an2 1166

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  3adant2l  1180  3adant2r  1181  syl3an2b  1406  syl3an2br  1409  fviunfun  7696  odi  8285  omass  8286  nndi  8329  nnmass  8330  omabslem  8353  winainf  10273  divsubdir  11491  divdiv32  11505  ltdiv2  11683  peano2uz  12462  irrmul  12535  supxrunb1  12874  fzoshftral  13324  ltdifltdiv  13374  axdc4uzlem  13521  expdiv  13651  bcval5  13849  ccats1val1OLD  14150  rediv  14659  imdiv  14666  absdiflt  14846  absdifle  14847  iseraltlem3  15212  retancl  15666  tanneg  15672  lcmgcdeq  16132  prmdvdsexpb  16236  dvdsprmpweqnn  16401  mulgaddcomlem  18468  mulginvcom  18470  pmtrfb  18811  lspssp  19979  mdetunilem7  21469  m2detleiblem3  21480  m2detleiblem4  21481  pmatcollpw  21632  pmatcollpwscmat  21642  chpmatply1  21683  chfacfscmulgsum  21711  chfacfpmmulcl  21712  chfacfpmmul0  21713  chfacfpmmulgsum  21715  chfacfpmmulgsum2  21716  cayhamlem1  21717  cpmadurid  21718  cpmadugsumlemC  21726  cpmadugsumlemF  21727  cpmadugsumfi  21728  cpmidgsum2  21730  islp2  21996  fmfg  22800  fmufil  22810  flffbas  22846  lmflf  22856  uffcfflf  22890  blres  23283  ncvsge0  24004  caucfil  24134  cmetcusp1  24204  deg1mul3  24967  quotval  25139  cusgr3vnbpr  27478  clwwlkinwwlk  28077  nvsge0  28699  hvsubass  29079  hvsubdistr2  29085  hvsubcan  29109  his2sub  29127  chlub  29544  spanunsni  29614  homco1  29836  homulass  29837  cnlnadjlem2  30103  adjmul  30127  chirredlem2  30426  atmd2  30435  mdsymlem5  30442  f1resrcmplf1dlem  32725  revpfxsfxrev  32744  climuzcnv  33296  pibt2  35274  f1ocan2fv  35571  isdrngo2  35802  atncvrN  37015  cvlatcvr1  37041  eluzrabdioph  40272  iocmbl  40688  rp-isfinite6  40751  ismnushort  41533  dvconstbi  41566  eelT11  41941  eelT12  41943  eelTT1  41944  eel0T1  41946  nn0digval  45562  dignn0flhalf  45580  sinhpcosh  46056  reseccl  46069  recsccl  46070  recotcl  46071  onetansqsecsq  46077