Доказательство

(1) состоит из одного шага подстановки:

And1 X & Y X // a ~> X, b ~> Y

(2) получается из (1) передвиганием на шаг вправо.

(3) состоит из одного шага подстановки:

And2 X & Y Y // a ~> X, b ~> Y

(4) получается из (3) передвиганием на шаг вправо.

(5) состоит из следующих шагов:

1)	And3	X (Y (X & Y))	// a ~> X, b ~> Y
2)	X, №1	Y (X & Y)	// MP
3)	Y, №2	X & Y	// MP

(6) состоит из следующих шагов:

1)	And3	Y (X (Y & X))	// a ~> Y, b ~> X
2)	Y, №1	X (Y & X)	// MP
3)	X, №2	Y & X	// MP

Доказательство

Составляем доказательство (2) следующим образом:

Строки доказательства X & Y X из MT_And_1.
Строки доказательства X & Y Y из MT_And_1.
Строки доказательства G₁, G₂,... G_β, X, Y Z из (1).

Составляем доказательство (1) следующим образом:

Строки доказательства X, Y X & Y из MT_And_1.
Строки доказательства G₁, G₂,... G_β, X & Y Z из (2).