Theorem syl3an2 1165

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adant2l  1180  3adant2r  1181  syl3an2b  1407  syl3an2br  1410  fviunfun  7899  odi  8516  omass  8517  nndi  8561  nnmass  8562  omabslem  8588  domtrfil  9128  domnsymfi  9136  sdomdomtrfi  9137  domsdomtrfi  9138  php  9143  php3  9145  f1finf1o  9185  findcard3  9195  winainf  10617  divsubdir  11847  divdiv32  11861  ltdiv2  12040  peano2uz  12826  irrmul  12899  supxrunb1  13246  fzoshftral  13715  ltdifltdiv  13766  axdc4uzlem  13918  expdiv  14048  bcval5  14253  rediv  15066  imdiv  15073  absdiflt  15253  absdifle  15254  iseraltlem3  15619  retancl  16079  tanneg  16085  difmod0  16226  lcmgcdeq  16551  prmdvdsexpb  16655  dvdsprmpweqnn  16825  mulgaddcomlem  19039  mulginvcom  19041  pmtrfb  19406  lspssp  20951  mdetunilem7  22574  m2detleiblem3  22585  m2detleiblem4  22586  pmatcollpw  22737  pmatcollpwscmat  22747  chpmatply1  22788  chfacfscmulgsum  22816  chfacfpmmulcl  22817  chfacfpmmul0  22818  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmadurid  22823  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cpmadugsumfi  22833  cpmidgsum2  22835  islp2  23101  fmfg  23905  fmufil  23915  flffbas  23951  lmflf  23961  uffcfflf  23995  blres  24387  ncvsge0  25121  caucfil  25251  cmetcusp1  25321  deg1mul3  26089  quotval  26268  ltonold  28269  cusgr3vnbpr  29521  clwwlkinwwlk  30127  nvsge0  30751  hvsubass  31131  hvsubdistr2  31137  hvsubcan  31161  his2sub  31179  chlub  31596  spanunsni  31666  homco1  31888  homulass  31889  cnlnadjlem2  32155  adjmul  32179  chirredlem2  32478  atmd2  32487  mdsymlem5  32494  f1resrcmplf1dlem  35261  revpfxsfxrev  35329  climuzcnv  35884  pibt2  37669  f1ocan2fv  37975  isdrngo2  38206  atncvrN  39688  cvlatcvr1  39714  eluzrabdioph  43160  iocmbl  43567  rp-isfinite6  43871  ismnushort  44654  dvconstbi  44687  eelT11  45059  eelT12  45061  eelTT1  45062  eel0T1  45064  nn0digval  48957  dignn0flhalf  48975  sinhpcosh  50096  reseccl  50109  recsccl  50110  recotcl  50111  onetansqsecsq  50117