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  7898  odi  8514  omass  8515  nndi  8559  nnmass  8560  omabslem  8586  domtrfil  9126  domnsymfi  9134  sdomdomtrfi  9135  domsdomtrfi  9136  php  9141  php3  9143  f1finf1o  9183  findcard3  9193  winainf  10617  divsubdir  11848  divdiv32  11863  ltdiv2  12042  peano2uz  12851  irrmul  12924  supxrunb1  13271  fzoshftral  13742  ltdifltdiv  13793  axdc4uzlem  13945  expdiv  14075  bcval5  14280  rediv  15093  imdiv  15100  absdiflt  15280  absdifle  15281  iseraltlem3  15646  retancl  16109  tanneg  16115  difmod0  16256  lcmgcdeq  16581  prmdvdsexpb  16686  dvdsprmpweqnn  16856  mulgaddcomlem  19073  mulginvcom  19075  pmtrfb  19440  lspssp  20983  mdetunilem7  22583  m2detleiblem3  22594  m2detleiblem4  22595  pmatcollpw  22746  pmatcollpwscmat  22756  chpmatply1  22797  chfacfscmulgsum  22825  chfacfpmmulcl  22826  chfacfpmmul0  22827  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadurid  22832  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cpmadugsumfi  22842  cpmidgsum2  22844  islp2  23110  fmfg  23914  fmufil  23924  flffbas  23960  lmflf  23970  uffcfflf  24004  blres  24396  ncvsge0  25120  caucfil  25250  cmetcusp1  25320  deg1mul3  26081  quotval  26258  ltonold  28253  cusgr3vnbpr  29505  clwwlkinwwlk  30110  nvsge0  30735  hvsubass  31115  hvsubdistr2  31121  hvsubcan  31145  his2sub  31163  chlub  31580  spanunsni  31650  homco1  31872  homulass  31873  cnlnadjlem2  32139  adjmul  32163  chirredlem2  32462  atmd2  32471  mdsymlem5  32478  f1resrcmplf1dlem  35229  revpfxsfxrev  35298  climuzcnv  35853  pibt2  37733  f1ocan2fv  38048  isdrngo2  38279  atncvrN  39761  cvlatcvr1  39787  eluzrabdioph  43234  iocmbl  43641  rp-isfinite6  43945  ismnushort  44728  dvconstbi  44761  eelT11  45133  eelT12  45135  eelTT1  45136  eel0T1  45138  nn0digval  49076  dignn0flhalf  49094  sinhpcosh  50215  reseccl  50228  recsccl  50229  recotcl  50230  onetansqsecsq  50236