 where 1, 2 and 4 are axioms and 3, 5 come from earlier lines by modus ponens. However, \(A\) is derivable from \(A\) (as assumption) in one obvious step, so the Deduction Theorem allows us to conclude that a proof of \(A \rightarrow A\) exists. (In fact, the formal proof of \(A \rightarrow A\) just presented is part of the constructive proof of the Deduction Theorem!)