Theorem id

Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT. Its associated inference, idi, requires no axioms for its proof, contrary to id. Note that the second occurrences of \( \varphi \) in Steps 1 and 2 may be simultaneously replaced by any wff \( \psi \), which may ease the understanding of the proof. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Conclusion
\( \vdash \varphi \rightarrow \varphi \)
Proof
l0
ax-1
\( \vdash \varphi \rightarrow \varphi \rightarrow \varphi \)
ax-1
\( \vdash \varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \)
mpd l0 _