1 ∀x;x=y⇒(x=z⇒y=z) Gen(x,I1)
2 ∀x;x=y⇒(x=z⇒y=z)⇒x+0=y⇒(x+0=z⇒y=z) Ax4(x,x+0,x=y⇒(x=z⇒y=z))
3 x+0=y⇒(x+0=z⇒y=z) MP(1,2)
4 ∀y x+0=y⇒(x+0=z⇒y=z) Gen(y,2)
5 ∀y x+0=y⇒(x+0=z⇒y=z)⇒ x+0=x⇒(x+0=z⇒x=z) Ax4(y,x,x+0=y⇒(x+0=z⇒y=z))
6 x+0=x⇒(x+0=z⇒x=z) MP(4,5)
7 x+0=z⇒x=z MP(I5,6)
8 ∀z x+0=z⇒x=z Gen(z,7)
9 (∀z x+0=z⇒x=z)⇒( x+0=x⇒x=x) Ax4(z,x,x+0=z⇒x=z))
10 ( x+0=x⇒x=x) MP(8,9)
11 x=x MP(-5,10)
12 ∀z x=y⇒(x=z⇒y=z) Gen(z,I1)
13 ∀z x=y⇒(x=z⇒y=z)⇒x=y⇒(x=x⇒y=x) Ax4(z,x,x=y⇒(x=z⇒y=z))
14 x=y⇒(x=x⇒y=x) MP(12,13)
15 x=y⇒(x=x⇒y=x)⇒(x=y⇒x=x)⇒(x=y⇒y=x) Ax2(x=y,x=x,y=x)
16 (x=y⇒x=x)⇒(x=y⇒y=x) MP(14,15)
17 x=x⇒(x=y⇒x=x) Ax1(x=x,x=y)
18 x=y⇒x=x MP(11,17)
19 x=y⇒y=x MP(18,16)
20 ∀x (x+y')=(x+y)' Gen(x,I6)
21 ∀x (x+y')=(x+y)'⇒(0'+y')=(0'+y)' Ax4(x,0', (x+y')=(x+y)')
22 (0'+y')=(0'+y)' MP(20,21)
23 ∀y (0'+y')=(0'+y)' Gen(y,22)
24 ∀(0'+y')=(0'+y)'⇒(0'+0')=(0'+0)' Ax4(y,0,(0+y')=(0+y)')
25 (0'+0')=(0'+0)' MP(23,24)
26 ∀x (x+0)=x Gen(y,I5)
27 ∀x (x+0)=x ⇒ (0'+0)=0' Ax4(x,0',(x+0)=x)
28 (0'+0)=0' MP(26,27)
29 ∀x (x=y⇒x'=y') Gen(x,I2)
30 ∀x (x=y⇒x'=y')⇒ ((0'+0)=y⇒(0'+0)'=y') Ax4((x,0'+0,x=y⇒x'=y'))
31 ((0'+0)=y⇒(0'+0)'=y') MP(29,30)
32 ∀y ((0'+0)=y⇒(0'+0)'=y') Gen(y,31)
33 ∀y (0'+0)=y⇒(0'+0)'=y')⇒((0'+0)=0'⇒(0'+0)'=0'') Ax4(y,0',(0'+0)=y⇒(0'+0)'=y')
34 ((0'+0)=0'⇒(0'+0)'=0'') MP(32,33)
35 (0'+0)'=0'' MP(28,34)
36 ∀x x=y⇒y=x Gen(x,19)
37 (∀x x=y⇒y=x)⇒( (0'+0')=y⇒y=(0'+0')) Ax4(x,(0'+0')(∀x x=y⇒y=x))
38 (0'+0')=y⇒y=(0'+0') MP(36,37)
39 ∀y (0'+0')=y⇒y=(0'+0') Gen(y,38)
40 ∀y (0'+0')=y⇒y=(0'+0') ⇒ ((0'+0')=(0'+0)'⇒(0'+0)'=(0'+0') Ax4(y,(0'+0)',(0'+0')=y⇒y=(0'+0'))
41 ((0'+0')=(0'+0)'⇒(0'+0)'=(0'+0') MP(39,40)
42 (0'+0)'=(0'+0') MP(25,41)
43 (∀z x=y⇒(x=z⇒y=z)) ⇒ x=y⇒(x=0''⇒y=0'') Ax4(z,0'',x=y⇒(x=z⇒y=z))
44 x=y⇒(x=0''⇒y=0'') MP(12,43)
45 ∀x x=y⇒(x=0''⇒y=0'') Gen(x,44)
46 ∀x x=y⇒(x=0''⇒y=0'')⇒( (0'+0)' =y⇒((0'+0)' =0''⇒y=0'')) Ax4(x,x,(0'+0)',x=y⇒(x=0''⇒y=0'') )
47 (0'+0)' =y⇒((0'+0)' =0''⇒y=0'') MP(45,46)
48 ∀y (0'+0)'=y⇒((0'+0)' =0''⇒y=0'') Gen(y,47)
49 ∀y (0'+0)' =y⇒((0'+0)' =0''⇒y=0'')⇒
((0'+0)' =(0'+0')⇒((0'+0)' =0''⇒(0'+0')=0'')) Ax4( y,(0'+0'),
(0'+0)' =y⇒((0'+0)' =0''⇒y=0''),)
50 (0'+0)' =(0'+0')⇒((0'+0)' =0''⇒(0'+0')=0'') MP(48,49)
51 (0'+0)' =0''⇒(0'+0')=0'' MP(42,50)
52 (0'+0')=0'' MP(35,51)
