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

Theorem sb8euOLDOLD 2301
 Description: Obsolete proof of sb8eu 2299 as of 8-Oct-2018. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
sb8eu.1
Assertion
Ref Expression
sb8euOLDOLD

Proof of Theorem sb8euOLDOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1674 . . . . 5
21sb8 2131 . . . 4
3 sbbi 2100 . . . . . 6
4 sb8eu.1 . . . . . . . 8
54nfsb 2153 . . . . . . 7
6 equsb3 2144 . . . . . . . 8
7 nfv 1674 . . . . . . . 8
86, 7nfxfr 1616 . . . . . . 7
95, 8nfbi 1869 . . . . . 6
103, 9nfxfr 1616 . . . . 5
11 nfv 1674 . . . . 5
12 sbequ 2074 . . . . 5
1310, 11, 12cbval 1978 . . . 4
14 equsb3 2144 . . . . . 6
1514sblbis 2103 . . . . 5
1615albii 1611 . . . 4
172, 13, 163bitri 271 . . 3
1817exbii 1635 . 2
19 df-eu 2264 . 2
20 df-eu 2264 . 2
2118, 19, 203bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:   wb 184  wal 1368  wex 1587  wnf 1590  wsb 1702  weu 2260 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator