Theorem zaddlass ≪ | index | src | ≫

theorem zaddlass (a b c: nat): $ a +Z (b +Z c) = b +Z (a +Z c) $;

Step	Hyp	Ref	Expression
1		eqtr3	a +Z b +Z c = a +Z (b +Z c) -> a +Z b +Z c = b +Z (a +Z c) -> a +Z (b +Z c) = b +Z (a +Z c)
2		zaddass	a +Z b +Z c = a +Z (b +Z c)
3	1, 2	ax_mp	a +Z b +Z c = b +Z (a +Z c) -> a +Z (b +Z c) = b +Z (a +Z c)
4		eqtr	a +Z b +Z c = b +Z a +Z c -> b +Z a +Z c = b +Z (a +Z c) -> a +Z b +Z c = b +Z (a +Z c)
5		zaddeq1	a +Z b = b +Z a -> a +Z b +Z c = b +Z a +Z c
6		zaddcom	a +Z b = b +Z a
7	5, 6	ax_mp	a +Z b +Z c = b +Z a +Z c
8	4, 7	ax_mp	b +Z a +Z c = b +Z (a +Z c) -> a +Z b +Z c = b +Z (a +Z c)
9		zaddass	b +Z a +Z c = b +Z (a +Z c)
10	8, 9	ax_mp	a +Z b +Z c = b +Z (a +Z c)
11	3, 10	ax_mp	a +Z (b +Z c) = b +Z (a +Z c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)