Theorem pm5.4

Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)

Conclusion

\( \vdash \varphi \rightarrow \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \psi \)

Proof

pm5.5

pm5.74i _