Theorem syl3an3 1164

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 1153	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3adant3l  1179  3adant3r  1180  syl3an3b  1404  syl3an3br  1407  disji  5057  ovmpox  7426  ovmpoga  7427  wrecseq123  8130  wfrlem14OLD  8153  dif1en  8945  domtrfil  8978  ssdomfi2  8983  domnsymfi  8986  sdomdomtrfi  8987  domsdomtrfi  8988  phplem2  8991  php  8993  php3  8995  unbnn2  9071  axdc3lem4  10209  axdclem2  10276  gruiin  10566  gruen  10568  divass  11651  ltmul2  11826  xleadd1  12989  xltadd2  12991  xlemul1  13024  xltmul2  13027  elfzo  13389  modcyc2  13627  faclbnd5  14012  relexprel  14750  subcn2  15304  mulcn2  15305  ndvdsp1  16120  gcddiv  16259  lcmneg  16308  lubel  18232  gsumccatsn  18482  mulgaddcom  18727  oddvdsi  19156  odcong  19157  odeq  19158  efgsp1  19343  lspsnss  20252  lindsmm2  21036  mulmarep1el  21721  mdetunilem4  21764  iuncld  22196  neips  22264  opnneip  22270  comppfsc  22683  hmeof1o2  22914  ordthmeo  22953  ufinffr  23080  elfm3  23101  utop3cls  23403  blcntrps  23565  blcntr  23566  neibl  23657  blnei  23658  metss  23664  stdbdmetval  23670  prdsms  23687  blval2  23718  lmmbr  24422  lmmbr2  24423  iscau2  24441  bcthlem1  24488  bcthlem3  24490  bcthlem4  24491  dvn2bss  25094  dvfsumrlim  25195  dvfsumrlim2  25196  cxpexpz  25822  cxpsub  25837  cxpcom  25892  relogbzexp  25926  1ewlk  28479  1pthon2ve  28518  upgr4cycl4dv4e  28549  konigsbergssiedgwpr  28613  dlwwlknondlwlknonf1o  28729  hvaddsub12  29400  hvaddsubass  29403  hvsubdistr1  29411  hvsubcan  29436  hhssnv  29626  spanunsni  29941  homco1  30163  homulass  30164  hoadddir  30166  hosubdi  30170  hoaddsubass  30177  hosubsub4  30180  lnopmi  30362  adjlnop  30448  mdsymlem5  30769  disjif  30917  disjif2  30920  ind0  31986  sigaclfu  32087  signstfvc  32553  bnj544  32874  bnj561  32883  bnj562  32884  bnj594  32892  swrdrevpfx  33078  satfvsuc  33323  satfvsucsuc  33327  clsint2  34518  ftc1anclem6  35855  isbnd2  35941  blbnd  35945  isdrngo2  36116  atnem0  37332  hlrelat5N  37415  ltrnel  38153  ltrnat  38154  ltrncnvat  38155  nnproddivdvdsd  40009  dvdsexpnn  40340  jm2.22  40817  jm2.23  40818  dvconstbi  41952  eelT11  42327  eelT12  42329  eelTT1  42330  eelT01  42331  eel0T1  42332  liminfvalxr  43324  rmfsupp  45710  mndpfsupp  45712  scmfsupp  45714  dignn0flhalflem2  45962  rrx2vlinest  46087  rrx2linesl  46089