Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sb8euOLD Structured version   Unicode version

Theorem sb8euOLD 2320
 Description: Obsolete proof of sb8eu 2319 as of 24-Aug-2019. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 8-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
sb8eu.1
Assertion
Ref Expression
sb8euOLD

Proof of Theorem sb8euOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1708 . . . . 5
21sb8 2168 . . . 4
3 equsb3 2177 . . . . . . 7
43sblbis 2146 . . . . . 6
5 sb8eu.1 . . . . . . . 8
65nfsb 2185 . . . . . . 7
7 nfv 1708 . . . . . . 7
86, 7nfbi 1935 . . . . . 6
94, 8nfxfr 1646 . . . . 5
10 nfv 1708 . . . . 5
11 sbequ 2118 . . . . 5
129, 10, 11cbval 2022 . . . 4
13 equsb3 2177 . . . . . 6
1413sblbis 2146 . . . . 5
1514albii 1641 . . . 4
162, 12, 153bitri 271 . . 3
1716exbii 1668 . 2
18 df-eu 2287 . 2
19 df-eu 2287 . 2
2017, 18, 193bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:   wb 184  wal 1393  wex 1613  wnf 1617  wsb 1740  weu 2283 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator