Theorem syl3an2 1170

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adant2l  1185  3adant2r  1186  syl3an2b  1412  syl3an2br  1415  fviunfun  7894  odi  8511  omass  8512  nndi  8556  nnmass  8557  omabslem  8583  domtrfil  9123  domnsymfi  9131  sdomdomtrfi  9132  domsdomtrfi  9133  php  9138  php3  9140  f1finf1o  9180  findcard3  9190  winainf  10615  divsubdir  11846  divdiv32  11861  ltdiv2  12040  peano2uz  12849  irrmul  12922  supxrunb1  13269  fzoshftral  13740  ltdifltdiv  13791  axdc4uzlem  13943  expdiv  14073  bcval5  14278  rediv  15091  imdiv  15098  absdiflt  15278  absdifle  15279  iseraltlem3  15644  retancl  16107  tanneg  16113  difmod0  16254  lcmgcdeq  16579  prmdvdsexpb  16684  dvdsprmpweqnn  16854  mulgaddcomlem  19071  mulginvcom  19073  pmtrfb  19438  lspssp  20985  mdetunilem7  22608  m2detleiblem3  22619  m2detleiblem4  22620  pmatcollpw  22771  pmatcollpwscmat  22781  chpmatply1  22822  chfacfscmulgsum  22850  chfacfpmmulcl  22851  chfacfpmmul0  22852  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmadurid  22857  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cpmadugsumfi  22867  cpmidgsum2  22869  islp2  23135  fmfg  23939  fmufil  23949  flffbas  23985  lmflf  23995  uffcfflf  24029  blres  24421  ncvsge0  25145  caucfil  25275  cmetcusp1  25345  deg1mul3  26106  quotval  26283  ltonold  28278  cusgr3vnbpr  29530  clwwlkinwwlk  30135  nvsge0  30760  hvsubass  31140  hvsubdistr2  31146  hvsubcan  31170  his2sub  31188  chlub  31605  spanunsni  31675  homco1  31897  homulass  31898  cnlnadjlem2  32164  adjmul  32188  chirredlem2  32487  atmd2  32496  mdsymlem5  32503  f1resrcmplf1dlem  35274  revpfxsfxrev  35351  climuzcnv  35906  pibt2  37786  f1ocan2fv  38101  isdrngo2  38332  atncvrN  39814  cvlatcvr1  39840  eluzrabdioph  43258  iocmbl  43665  rp-isfinite6  43969  ismnushort  44752  dvconstbi  44785  eelT11  45157  eelT12  45159  eelTT1  45160  eel0T1  45162  nn0digval  49098  dignn0flhalf  49116  sinhpcosh  50237  reseccl  50250  recsccl  50251  recotcl  50252  onetansqsecsq  50258