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  7926  odi  8546  omass  8547  nndi  8590  nnmass  8591  omabslem  8617  domtrfil  9162  domnsymfi  9170  sdomdomtrfi  9171  domsdomtrfi  9172  php  9177  php3  9179  f1finf1o  9223  findcard3  9236  winainf  10654  divsubdir  11883  divdiv32  11897  ltdiv2  12076  peano2uz  12867  irrmul  12940  supxrunb1  13286  fzoshftral  13752  ltdifltdiv  13803  axdc4uzlem  13955  expdiv  14085  bcval5  14290  rediv  15104  imdiv  15111  absdiflt  15291  absdifle  15292  iseraltlem3  15657  retancl  16117  tanneg  16123  difmod0  16264  lcmgcdeq  16589  prmdvdsexpb  16693  dvdsprmpweqnn  16863  mulgaddcomlem  19036  mulginvcom  19038  pmtrfb  19402  lspssp  20901  mdetunilem7  22512  m2detleiblem3  22523  m2detleiblem4  22524  pmatcollpw  22675  pmatcollpwscmat  22685  chpmatply1  22726  chfacfscmulgsum  22754  chfacfpmmulcl  22755  chfacfpmmul0  22756  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmadurid  22761  cpmadugsumlemC  22769  cpmadugsumlemF  22770  cpmadugsumfi  22771  cpmidgsum2  22773  islp2  23039  fmfg  23843  fmufil  23853  flffbas  23889  lmflf  23899  uffcfflf  23933  blres  24326  ncvsge0  25060  caucfil  25190  cmetcusp1  25260  deg1mul3  26028  quotval  26207  sltonold  28169  cusgr3vnbpr  29370  clwwlkinwwlk  29976  nvsge0  30600  hvsubass  30980  hvsubdistr2  30986  hvsubcan  31010  his2sub  31028  chlub  31445  spanunsni  31515  homco1  31737  homulass  31738  cnlnadjlem2  32004  adjmul  32028  chirredlem2  32327  atmd2  32336  mdsymlem5  32343  f1resrcmplf1dlem  35083  revpfxsfxrev  35110  climuzcnv  35665  pibt2  37412  f1ocan2fv  37728  isdrngo2  37959  atncvrN  39315  cvlatcvr1  39341  eluzrabdioph  42801  iocmbl  43209  rp-isfinite6  43514  ismnushort  44297  dvconstbi  44330  eelT11  44703  eelT12  44705  eelTT1  44706  eel0T1  44708  nn0digval  48593  dignn0flhalf  48611  sinhpcosh  49733  reseccl  49746  recsccl  49747  recotcl  49748  onetansqsecsq  49754