v1

|- A→A

Důkaz

Vyjdu z

|- A→[(A→A)→A]→[(A→(A→A))→(A→A)]

To je instance A2 (A→(B→C))→[(A→B)→(A→C)], kde

A ~ A
B ~ A→A
C ~ A

Dále

|- A→[(A→A)→A]

je instance A1 (A→(B→A)), kde

A ~ A
B ~ (A→A)

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