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  7891  odi  8507  omass  8508  nndi  8552  nnmass  8553  omabslem  8579  domtrfil  9119  domnsymfi  9127  sdomdomtrfi  9128  domsdomtrfi  9129  php  9134  php3  9136  f1finf1o  9176  findcard3  9186  winainf  10608  divsubdir  11839  divdiv32  11854  ltdiv2  12033  peano2uz  12842  irrmul  12915  supxrunb1  13262  fzoshftral  13733  ltdifltdiv  13784  axdc4uzlem  13936  expdiv  14066  bcval5  14271  rediv  15084  imdiv  15091  absdiflt  15271  absdifle  15272  iseraltlem3  15637  retancl  16100  tanneg  16106  difmod0  16247  lcmgcdeq  16572  prmdvdsexpb  16677  dvdsprmpweqnn  16847  mulgaddcomlem  19064  mulginvcom  19066  pmtrfb  19431  lspssp  20974  mdetunilem7  22593  m2detleiblem3  22604  m2detleiblem4  22605  pmatcollpw  22756  pmatcollpwscmat  22766  chpmatply1  22807  chfacfscmulgsum  22835  chfacfpmmulcl  22836  chfacfpmmul0  22837  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadurid  22842  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cpmadugsumfi  22852  cpmidgsum2  22854  islp2  23120  fmfg  23924  fmufil  23934  flffbas  23970  lmflf  23980  uffcfflf  24014  blres  24406  ncvsge0  25130  caucfil  25260  cmetcusp1  25330  deg1mul3  26091  quotval  26269  ltonold  28267  cusgr3vnbpr  29519  clwwlkinwwlk  30125  nvsge0  30750  hvsubass  31130  hvsubdistr2  31136  hvsubcan  31160  his2sub  31178  chlub  31595  spanunsni  31665  homco1  31887  homulass  31888  cnlnadjlem2  32154  adjmul  32178  chirredlem2  32477  atmd2  32486  mdsymlem5  32493  f1resrcmplf1dlem  35245  revpfxsfxrev  35314  climuzcnv  35869  pibt2  37747  f1ocan2fv  38062  isdrngo2  38293  atncvrN  39775  cvlatcvr1  39801  eluzrabdioph  43252  iocmbl  43659  rp-isfinite6  43963  ismnushort  44746  dvconstbi  44779  eelT11  45151  eelT12  45153  eelTT1  45154  eel0T1  45156  nn0digval  49088  dignn0flhalf  49106  sinhpcosh  50227  reseccl  50240  recsccl  50241  recotcl  50242  onetansqsecsq  50248