В доказательстве метатеоремы дедукции мы рассмотрели два варианта: когда среди наших аксиом
есть аксиомы Imp1 и Imp2 и когда среди наших аксиом есть аксиомы Imp1 и Imp2'. То есть, эта
метатеорема верна и при том, и при другом выборе аксиом. Помимо них в доказательстве используются
только те аксиомы, которые пришли вместе с исходным доказательством 
R
Более того, в последующих главах будут использоваться не аксиомы Imp1, Imp2, Imp2', а теорема дедукции, которая из них получается. Поэтому, в принципе, можно саму теорему дедукции считать аксиомой (или правилом вывода), а аксиомы Imp1/Imp2 исключить.
До сих пор мы не определились с выбором, какую из аксиом использовать: Imp2 или Imp2'. Во всех рассуждениях мы рассматривали оба варианта. Теперь мы докажем, что это не имеет значения. А точнее так: если принять за аксиомы Imp1 и Imp2, то можно будет доказать Imp2' как теорему. А если, наоборот, принять за аксиомы Imp1 и Imp2', то можно будет доказать как теорему Imp2. Получается, что эти два варианта КИВ в конечном счете приведут к одним и тем же доказанным формулам. Вот вам один из примеров, когда есть два взаимозаменяемых варианта КИВ.
Еще раз напомню аксиомы:
Imp2:
Imp2':
Возьмем в качестве аксиомы Imp2. Поскольку аксиома - формула доказанная, то можно написать:
ab ((a(bc))(ac))
Теперь передвинем значок
ab ((a(bc))(ac))
(a(bc))(ac)
ac
Переставим местами гипотезы
ac
Теперь передвинем значок
(ab)(ac)
a(bc) (ab)(ac)
- получилась Imp2' как теорема.
Аналогично можно получить Imp2 из Imp2'. Достаточно выписать все те же самые формулы, только в обратном порядке.
Далее для ясности будем считать Imp2 аксиомой, а Imp2' - теоремой.