Metamath Proof Explorer

Theorem naddass

Description: Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddass Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 oveq1 Could not format ( a = x -> ( a +no b ) = ( x +no b ) ) : No typesetting found for |- ( a = x -> ( a +no b ) = ( x +no b ) ) with typecode |-
2 1 oveq1d Could not format ( a = x -> ( ( a +no b ) +no c ) = ( ( x +no b ) +no c ) ) : No typesetting found for |- ( a = x -> ( ( a +no b ) +no c ) = ( ( x +no b ) +no c ) ) with typecode |-
3 oveq1 Could not format ( a = x -> ( a +no ( b +no c ) ) = ( x +no ( b +no c ) ) ) : No typesetting found for |- ( a = x -> ( a +no ( b +no c ) ) = ( x +no ( b +no c ) ) ) with typecode |-
4 2 3 eqeq12d Could not format ( a = x -> ( ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) <-> ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) ) ) : No typesetting found for |- ( a = x -> ( ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) <-> ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) ) ) with typecode |-
5 oveq2 Could not format ( b = y -> ( x +no b ) = ( x +no y ) ) : No typesetting found for |- ( b = y -> ( x +no b ) = ( x +no y ) ) with typecode |-
6 5 oveq1d Could not format ( b = y -> ( ( x +no b ) +no c ) = ( ( x +no y ) +no c ) ) : No typesetting found for |- ( b = y -> ( ( x +no b ) +no c ) = ( ( x +no y ) +no c ) ) with typecode |-
7 oveq1 Could not format ( b = y -> ( b +no c ) = ( y +no c ) ) : No typesetting found for |- ( b = y -> ( b +no c ) = ( y +no c ) ) with typecode |-
8 7 oveq2d Could not format ( b = y -> ( x +no ( b +no c ) ) = ( x +no ( y +no c ) ) ) : No typesetting found for |- ( b = y -> ( x +no ( b +no c ) ) = ( x +no ( y +no c ) ) ) with typecode |-
9 6 8 eqeq12d Could not format ( b = y -> ( ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) <-> ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) ) ) : No typesetting found for |- ( b = y -> ( ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) <-> ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) ) ) with typecode |-
10 oveq2 Could not format ( c = z -> ( ( x +no y ) +no c ) = ( ( x +no y ) +no z ) ) : No typesetting found for |- ( c = z -> ( ( x +no y ) +no c ) = ( ( x +no y ) +no z ) ) with typecode |-
11 oveq2 Could not format ( c = z -> ( y +no c ) = ( y +no z ) ) : No typesetting found for |- ( c = z -> ( y +no c ) = ( y +no z ) ) with typecode |-
12 11 oveq2d Could not format ( c = z -> ( x +no ( y +no c ) ) = ( x +no ( y +no z ) ) ) : No typesetting found for |- ( c = z -> ( x +no ( y +no c ) ) = ( x +no ( y +no z ) ) ) with typecode |-
13 10 12 eqeq12d Could not format ( c = z -> ( ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) ) : No typesetting found for |- ( c = z -> ( ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) ) with typecode |-
14 oveq1 Could not format ( a = x -> ( a +no y ) = ( x +no y ) ) : No typesetting found for |- ( a = x -> ( a +no y ) = ( x +no y ) ) with typecode |-
15 14 oveq1d Could not format ( a = x -> ( ( a +no y ) +no z ) = ( ( x +no y ) +no z ) ) : No typesetting found for |- ( a = x -> ( ( a +no y ) +no z ) = ( ( x +no y ) +no z ) ) with typecode |-
16 oveq1 Could not format ( a = x -> ( a +no ( y +no z ) ) = ( x +no ( y +no z ) ) ) : No typesetting found for |- ( a = x -> ( a +no ( y +no z ) ) = ( x +no ( y +no z ) ) ) with typecode |-
17 15 16 eqeq12d Could not format ( a = x -> ( ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) ) : No typesetting found for |- ( a = x -> ( ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) ) with typecode |-
18 oveq2 Could not format ( b = y -> ( a +no b ) = ( a +no y ) ) : No typesetting found for |- ( b = y -> ( a +no b ) = ( a +no y ) ) with typecode |-
19 18 oveq1d Could not format ( b = y -> ( ( a +no b ) +no z ) = ( ( a +no y ) +no z ) ) : No typesetting found for |- ( b = y -> ( ( a +no b ) +no z ) = ( ( a +no y ) +no z ) ) with typecode |-
20 oveq1 Could not format ( b = y -> ( b +no z ) = ( y +no z ) ) : No typesetting found for |- ( b = y -> ( b +no z ) = ( y +no z ) ) with typecode |-
21 20 oveq2d Could not format ( b = y -> ( a +no ( b +no z ) ) = ( a +no ( y +no z ) ) ) : No typesetting found for |- ( b = y -> ( a +no ( b +no z ) ) = ( a +no ( y +no z ) ) ) with typecode |-
22 19 21 eqeq12d Could not format ( b = y -> ( ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) <-> ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) ) ) : No typesetting found for |- ( b = y -> ( ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) <-> ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) ) ) with typecode |-
23 5 oveq1d Could not format ( b = y -> ( ( x +no b ) +no z ) = ( ( x +no y ) +no z ) ) : No typesetting found for |- ( b = y -> ( ( x +no b ) +no z ) = ( ( x +no y ) +no z ) ) with typecode |-
24 20 oveq2d Could not format ( b = y -> ( x +no ( b +no z ) ) = ( x +no ( y +no z ) ) ) : No typesetting found for |- ( b = y -> ( x +no ( b +no z ) ) = ( x +no ( y +no z ) ) ) with typecode |-
25 23 24 eqeq12d Could not format ( b = y -> ( ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) ) : No typesetting found for |- ( b = y -> ( ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) ) with typecode |-
26 oveq2 Could not format ( c = z -> ( ( a +no y ) +no c ) = ( ( a +no y ) +no z ) ) : No typesetting found for |- ( c = z -> ( ( a +no y ) +no c ) = ( ( a +no y ) +no z ) ) with typecode |-
27 11 oveq2d Could not format ( c = z -> ( a +no ( y +no c ) ) = ( a +no ( y +no z ) ) ) : No typesetting found for |- ( c = z -> ( a +no ( y +no c ) ) = ( a +no ( y +no z ) ) ) with typecode |-
28 26 27 eqeq12d Could not format ( c = z -> ( ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) <-> ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) ) ) : No typesetting found for |- ( c = z -> ( ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) <-> ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) ) ) with typecode |-
29 oveq1 Could not format ( a = A -> ( a +no b ) = ( A +no b ) ) : No typesetting found for |- ( a = A -> ( a +no b ) = ( A +no b ) ) with typecode |-
30 29 oveq1d Could not format ( a = A -> ( ( a +no b ) +no c ) = ( ( A +no b ) +no c ) ) : No typesetting found for |- ( a = A -> ( ( a +no b ) +no c ) = ( ( A +no b ) +no c ) ) with typecode |-
31 oveq1 Could not format ( a = A -> ( a +no ( b +no c ) ) = ( A +no ( b +no c ) ) ) : No typesetting found for |- ( a = A -> ( a +no ( b +no c ) ) = ( A +no ( b +no c ) ) ) with typecode |-
32 30 31 eqeq12d Could not format ( a = A -> ( ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) <-> ( ( A +no b ) +no c ) = ( A +no ( b +no c ) ) ) ) : No typesetting found for |- ( a = A -> ( ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) <-> ( ( A +no b ) +no c ) = ( A +no ( b +no c ) ) ) ) with typecode |-
33 oveq2 Could not format ( b = B -> ( A +no b ) = ( A +no B ) ) : No typesetting found for |- ( b = B -> ( A +no b ) = ( A +no B ) ) with typecode |-
34 33 oveq1d Could not format ( b = B -> ( ( A +no b ) +no c ) = ( ( A +no B ) +no c ) ) : No typesetting found for |- ( b = B -> ( ( A +no b ) +no c ) = ( ( A +no B ) +no c ) ) with typecode |-
35 oveq1 Could not format ( b = B -> ( b +no c ) = ( B +no c ) ) : No typesetting found for |- ( b = B -> ( b +no c ) = ( B +no c ) ) with typecode |-
36 35 oveq2d Could not format ( b = B -> ( A +no ( b +no c ) ) = ( A +no ( B +no c ) ) ) : No typesetting found for |- ( b = B -> ( A +no ( b +no c ) ) = ( A +no ( B +no c ) ) ) with typecode |-
37 34 36 eqeq12d Could not format ( b = B -> ( ( ( A +no b ) +no c ) = ( A +no ( b +no c ) ) <-> ( ( A +no B ) +no c ) = ( A +no ( B +no c ) ) ) ) : No typesetting found for |- ( b = B -> ( ( ( A +no b ) +no c ) = ( A +no ( b +no c ) ) <-> ( ( A +no B ) +no c ) = ( A +no ( B +no c ) ) ) ) with typecode |-
38 oveq2 Could not format ( c = C -> ( ( A +no B ) +no c ) = ( ( A +no B ) +no C ) ) : No typesetting found for |- ( c = C -> ( ( A +no B ) +no c ) = ( ( A +no B ) +no C ) ) with typecode |-
39 oveq2 Could not format ( c = C -> ( B +no c ) = ( B +no C ) ) : No typesetting found for |- ( c = C -> ( B +no c ) = ( B +no C ) ) with typecode |-
40 39 oveq2d Could not format ( c = C -> ( A +no ( B +no c ) ) = ( A +no ( B +no C ) ) ) : No typesetting found for |- ( c = C -> ( A +no ( B +no c ) ) = ( A +no ( B +no C ) ) ) with typecode |-
41 38 40 eqeq12d Could not format ( c = C -> ( ( ( A +no B ) +no c ) = ( A +no ( B +no c ) ) <-> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) ) : No typesetting found for |- ( c = C -> ( ( ( A +no B ) +no c ) = ( A +no ( B +no c ) ) <-> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) ) with typecode |-
42 simpr21 Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) ) with typecode |-
43 eleq1 Could not format ( ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) -> ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) ) : No typesetting found for |- ( ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) -> ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) ) with typecode |-
44 43 ralimi Could not format ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) -> A. x e. a ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) ) : No typesetting found for |- ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) -> A. x e. a ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) ) with typecode |-
45 ralbi Could not format ( A. x e. a ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) -> ( A. x e. a ( ( x +no b ) +no c ) e. w <-> A. x e. a ( x +no ( b +no c ) ) e. w ) ) : No typesetting found for |- ( A. x e. a ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) -> ( A. x e. a ( ( x +no b ) +no c ) e. w <-> A. x e. a ( x +no ( b +no c ) ) e. w ) ) with typecode |-
46 42 44 45 3syl Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. x e. a ( ( x +no b ) +no c ) e. w <-> A. x e. a ( x +no ( b +no c ) ) e. w ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. x e. a ( ( x +no b ) +no c ) e. w <-> A. x e. a ( x +no ( b +no c ) ) e. w ) ) with typecode |-
47 simpr23 Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) with typecode |-
48 eleq1 Could not format ( ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) -> ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) ) : No typesetting found for |- ( ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) -> ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) ) with typecode |-
49 48 ralimi Could not format ( A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) -> A. y e. b ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) ) : No typesetting found for |- ( A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) -> A. y e. b ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) ) with typecode |-
50 ralbi Could not format ( A. y e. b ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) -> ( A. y e. b ( ( a +no y ) +no c ) e. w <-> A. y e. b ( a +no ( y +no c ) ) e. w ) ) : No typesetting found for |- ( A. y e. b ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) -> ( A. y e. b ( ( a +no y ) +no c ) e. w <-> A. y e. b ( a +no ( y +no c ) ) e. w ) ) with typecode |-
51 47 49 50 3syl Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. y e. b ( ( a +no y ) +no c ) e. w <-> A. y e. b ( a +no ( y +no c ) ) e. w ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. y e. b ( ( a +no y ) +no c ) e. w <-> A. y e. b ( a +no ( y +no c ) ) e. w ) ) with typecode |-
52 simpr3 Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) with typecode |-
53 eleq1 Could not format ( ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) -> ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) ) : No typesetting found for |- ( ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) -> ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) ) with typecode |-
54 53 ralimi Could not format ( A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) -> A. z e. c ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) ) : No typesetting found for |- ( A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) -> A. z e. c ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) ) with typecode |-
55 ralbi Could not format ( A. z e. c ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) -> ( A. z e. c ( ( a +no b ) +no z ) e. w <-> A. z e. c ( a +no ( b +no z ) ) e. w ) ) : No typesetting found for |- ( A. z e. c ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) -> ( A. z e. c ( ( a +no b ) +no z ) e. w <-> A. z e. c ( a +no ( b +no z ) ) e. w ) ) with typecode |-
56 52 54 55 3syl Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. z e. c ( ( a +no b ) +no z ) e. w <-> A. z e. c ( a +no ( b +no z ) ) e. w ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. z e. c ( ( a +no b ) +no z ) e. w <-> A. z e. c ( a +no ( b +no z ) ) e. w ) ) with typecode |-
57 46 51 56 3anbi123d Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) <-> ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) <-> ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) ) ) with typecode |-
58 57 rabbidv Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } = { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } = { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) with typecode |-
59 58 inteqd Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) with typecode |-
60 naddasslem1 Could not format ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( a +no b ) +no c ) = |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( a +no b ) +no c ) = |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } ) with typecode |-
61 60 adantr Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( a +no b ) +no c ) = |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( a +no b ) +no c ) = |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } ) with typecode |-
62 naddasslem2 Could not format ( ( a e. On /\ b e. On /\ c e. On ) -> ( a +no ( b +no c ) ) = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On /\ c e. On ) -> ( a +no ( b +no c ) ) = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) with typecode |-
63 62 adantr Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( a +no ( b +no c ) ) = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( a +no ( b +no c ) ) = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } ) with typecode |-
64 59 61 63 3eqtr4d Could not format ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) ) with typecode |-
65 64 ex Could not format ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) -> ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) -> ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) ) ) with typecode |-
66 4 9 13 17 22 25 28 32 37 41 65 on3ind Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) with typecode |-