Theorem pm2.43

Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of [WhiteheadRussell] p. 106. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.)

Conclusion
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
Proof
pm2.27
a2i _