00.mm

d4::pa_ax3         |- = x + x 0
d5::ax-1           |- implies
                      = x + x 0
                      implies = y + y 0 = x + x 0
d3:d4,d5:ax-mp          |- implies = y + y 0 = x + x 0
3:d3:alpha_2       |- implies = y + y 0 forall x = x + x 0

d6::pa_ax3         |- = y + y 0
5:d6,3:ax-mp |- forall x = x + x 0


q1::all_elim       |- implies
                      forall x = x + x 0
                      forall
                      x
                      implies = x 0 = x + x 0
d1:5,q1:ax-mp      |- forall
                      x
                      implies = x 0 = x + x 0

u1::eq-refl        |- = 0 0


x1::df-an          |- iff
                      and = x 0 = 0 0
                      not implies = x 0 not = 0 0
x2::bi2            |- implies
                      iff
                      and = x 0 = 0 0
                      not implies = x 0 not = 0 0
                      implies
                      not implies = x 0 not = 0 0
                      and = x 0 = 0 0
x3:x1,x2:ax-mp     |- implies
                      not implies = x 0 not = 0 0
                      and = x 0 = 0 0


w1::eq-binop       |- implies and = x 0 = 0 0 = + x 0 + 0 0




t1::eq-congr       |- implies
                      and = x 0 = + x 0 + 0 0
                      iff = x + x 0 = 0 + 0 0


!d7::              |- implies
                      = x 0
                      iff = x + x 0 = 0 + 0 0
d2:d7:all_elim3    |- implies
                      forall
                      x
                      implies = x 0 = x + x 0
                      = 0 + 0 0
qed:d1,d2:ax-mp |- = 0 + 0 0