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  7923  odi  8543  omass  8544  nndi  8587  nnmass  8588  omabslem  8614  domtrfil  9156  domnsymfi  9164  sdomdomtrfi  9165  domsdomtrfi  9166  php  9171  php3  9173  f1finf1o  9216  findcard3  9229  winainf  10647  divsubdir  11876  divdiv32  11890  ltdiv2  12069  peano2uz  12860  irrmul  12933  supxrunb1  13279  fzoshftral  13745  ltdifltdiv  13796  axdc4uzlem  13948  expdiv  14078  bcval5  14283  rediv  15097  imdiv  15104  absdiflt  15284  absdifle  15285  iseraltlem3  15650  retancl  16110  tanneg  16116  difmod0  16257  lcmgcdeq  16582  prmdvdsexpb  16686  dvdsprmpweqnn  16856  mulgaddcomlem  19029  mulginvcom  19031  pmtrfb  19395  lspssp  20894  mdetunilem7  22505  m2detleiblem3  22516  m2detleiblem4  22517  pmatcollpw  22668  pmatcollpwscmat  22678  chpmatply1  22719  chfacfscmulgsum  22747  chfacfpmmulcl  22748  chfacfpmmul0  22749  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadurid  22754  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cpmadugsumfi  22764  cpmidgsum2  22766  islp2  23032  fmfg  23836  fmufil  23846  flffbas  23882  lmflf  23892  uffcfflf  23926  blres  24319  ncvsge0  25053  caucfil  25183  cmetcusp1  25253  deg1mul3  26021  quotval  26200  sltonold  28162  cusgr3vnbpr  29363  clwwlkinwwlk  29969  nvsge0  30593  hvsubass  30973  hvsubdistr2  30979  hvsubcan  31003  his2sub  31021  chlub  31438  spanunsni  31508  homco1  31730  homulass  31731  cnlnadjlem2  31997  adjmul  32021  chirredlem2  32320  atmd2  32329  mdsymlem5  32336  f1resrcmplf1dlem  35076  revpfxsfxrev  35103  climuzcnv  35658  pibt2  37405  f1ocan2fv  37721  isdrngo2  37952  atncvrN  39308  cvlatcvr1  39334  eluzrabdioph  42794  iocmbl  43202  rp-isfinite6  43507  ismnushort  44290  dvconstbi  44323  eelT11  44696  eelT12  44698  eelTT1  44699  eel0T1  44701  nn0digval  48589  dignn0flhalf  48607  sinhpcosh  49729  reseccl  49742  recsccl  49743  recotcl  49744  onetansqsecsq  49750