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  7877  odi  8494  omass  8495  nndi  8538  nnmass  8539  omabslem  8565  domtrfil  9101  domnsymfi  9109  sdomdomtrfi  9110  domsdomtrfi  9111  php  9116  php3  9118  f1finf1o  9157  findcard3  9167  winainf  10585  divsubdir  11815  divdiv32  11829  ltdiv2  12008  peano2uz  12799  irrmul  12872  supxrunb1  13218  fzoshftral  13687  ltdifltdiv  13738  axdc4uzlem  13890  expdiv  14020  bcval5  14225  rediv  15038  imdiv  15045  absdiflt  15225  absdifle  15226  iseraltlem3  15591  retancl  16051  tanneg  16057  difmod0  16198  lcmgcdeq  16523  prmdvdsexpb  16627  dvdsprmpweqnn  16797  mulgaddcomlem  19010  mulginvcom  19012  pmtrfb  19378  lspssp  20922  mdetunilem7  22534  m2detleiblem3  22545  m2detleiblem4  22546  pmatcollpw  22697  pmatcollpwscmat  22707  chpmatply1  22748  chfacfscmulgsum  22776  chfacfpmmulcl  22777  chfacfpmmul0  22778  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmadurid  22783  cpmadugsumlemC  22791  cpmadugsumlemF  22792  cpmadugsumfi  22793  cpmidgsum2  22795  islp2  23061  fmfg  23865  fmufil  23875  flffbas  23911  lmflf  23921  uffcfflf  23955  blres  24347  ncvsge0  25081  caucfil  25211  cmetcusp1  25281  deg1mul3  26049  quotval  26228  sltonold  28199  cusgr3vnbpr  29415  clwwlkinwwlk  30018  nvsge0  30642  hvsubass  31022  hvsubdistr2  31028  hvsubcan  31052  his2sub  31070  chlub  31487  spanunsni  31557  homco1  31779  homulass  31780  cnlnadjlem2  32046  adjmul  32070  chirredlem2  32369  atmd2  32378  mdsymlem5  32385  f1resrcmplf1dlem  35096  revpfxsfxrev  35158  climuzcnv  35713  pibt2  37457  f1ocan2fv  37773  isdrngo2  38004  atncvrN  39360  cvlatcvr1  39386  eluzrabdioph  42845  iocmbl  43252  rp-isfinite6  43557  ismnushort  44340  dvconstbi  44373  eelT11  44745  eelT12  44747  eelTT1  44748  eel0T1  44750  nn0digval  48638  dignn0flhalf  48656  sinhpcosh  49778  reseccl  49791  recsccl  49792  recotcl  49793  onetansqsecsq  49799