Theorem pm2.43i

Inference absorbing redundant antecedent. Inference associated with pm2.43. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)

Hypothesis
pm2.43i.1
\( \vdash \varphi \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
id
\( \vdash \varphi \rightarrow \varphi \)
pm2.43i.1
\( \vdash \varphi \rightarrow \varphi \rightarrow \psi \)
mpd l0 _