|- A→A
Vyjdu z
|- A→[(A→A)→A]→[(A→(A→A))→(A→A)]
To je instance A2 (A→(B→C))→[(A→B)→(A→C)], kde
Dále
|- A→[(A→A)→A]
je instance A1 (A→(B→A)), kde
Použiju pravidlo modus ponens
A->((A->A)->A) A->((A->A)->A)->[(A->(A->A))->(A->A)] --------------------------------------------------------- (A->(A->A))->(A->A)
Tedy
|- (A→(A→A))→(A→A)
Nyní použiju pro modus ponens další instanci A1, tentokrát
|- (A→(A→A))
(A->(A->A)) (A->(A->A))->(A->A) ------------------------------------ (A->A)
A výsledkem je tvrzení v1
|- A→A
QED