Theorem syl3an3 1165

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

Ref	Expression
syl3an3.1	⊢ (𝜑 → 𝜃)
syl3an3.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 ⊢ (𝜑 → 𝜃)
2	1	3anim3i 1154	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.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:  3adant3l  1181  3adant3r  1182  syl3an3b  1407  syl3an3br  1410  disji  5083  ovmpox  7511  ovmpoga  7512  wrecseq123  8255  dif1en  9086  domtrfil  9116  ssdomfi2  9121  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  phplem2  9129  php  9131  php3  9133  findcard3  9183  unbnn2  9197  axdc3lem4  10363  axdclem2  10430  gruiin  10721  gruen  10723  divass  11814  ltmul2  11992  xleadd1  13170  xltadd2  13172  xlemul1  13205  xltmul2  13208  elfzo  13577  modcyc2  13827  faclbnd5  14221  relexprel  14962  subcn2  15518  mulcn2  15519  ndvdsp1  16338  gcddiv  16478  lcmneg  16530  lubel  18437  mndpfsupp  18692  gsumccatsn  18768  mulgaddcom  19028  oddvdsi  19477  odcong  19478  odeq  19479  efgsp1  19666  lspsnss  20941  rnglidlrng  21202  lindsmm2  21784  mulmarep1el  22516  mdetunilem4  22559  iuncld  22989  neips  23057  opnneip  23063  comppfsc  23476  hmeof1o2  23707  ordthmeo  23746  ufinffr  23873  elfm3  23894  utop3cls  24195  blcntrps  24356  blcntr  24357  neibl  24445  blnei  24446  metss  24452  stdbdmetval  24458  prdsms  24475  blval2  24506  lmmbr  25214  lmmbr2  25215  iscau2  25233  bcthlem1  25280  bcthlem3  25282  bcthlem4  25283  dvn2bss  25888  dvfsumrlim  25994  dvfsumrlim2  25995  cxpexpz  26632  cxpsub  26647  cxpcom  26704  relogbzexp  26742  ltsubs1  28072  1ewlk  30190  1pthon2ve  30229  upgr4cycl4dv4e  30260  konigsbergssiedgwpr  30324  dlwwlknondlwlknonf1o  30440  hvaddsub12  31113  hvaddsubass  31116  hvsubdistr1  31124  hvsubcan  31149  hhssnv  31339  spanunsni  31654  homco1  31876  homulass  31877  hoadddir  31879  hosubdi  31883  hoaddsubass  31890  hosubsub4  31893  lnopmi  32075  adjlnop  32161  mdsymlem5  32482  disjif  32653  disjif2  32656  ind0  32937  sigaclfu  34276  signstfvc  34731  bnj544  35050  bnj561  35059  bnj562  35060  bnj594  35068  fineqvnttrclselem3  35279  swrdrevpfx  35311  satfvsuc  35555  satfvsucsuc  35559  clsint2  36523  weiunso  36660  weiunwe  36663  ftc1anclem6  37899  isbnd2  37984  blbnd  37988  isdrngo2  38159  atnem0  39578  hlrelat5N  39661  ltrnel  40399  ltrnat  40400  ltrncnvat  40401  nnproddivdvdsd  42254  dvdsexpnn  42588  jm2.22  43237  jm2.23  43238  dvconstbi  44575  eelT11  44947  eelT12  44949  eelTT1  44950  eelT01  44951  eel0T1  44952  liminfvalxr  46027  grlimprclnbgr  48242  rmfsupp  48619  scmfsupp  48621  dignn0flhalflem2  48862  rrx2vlinest  48987  rrx2linesl  48989