Theorem rb-imdf

The definition of implication, in terms of \/ and -.. (Contributed by Anthony Hart, 17-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg (\neg (\neg (\varphi \rightarrow \psi) \vee (\neg \varphi \vee \psi)) \vee \neg (\neg (\neg \varphi \vee \psi) \vee (\varphi \rightarrow \psi))) \)
Proof
l0
imor
\( \vdash \varphi \rightarrow \psi \leftrightarrow \neg \varphi \vee \psi \)
rb-bijust
\( \vdash \varphi \rightarrow \psi \leftrightarrow \neg \varphi \vee \psi \leftrightarrow \neg (\neg (\neg (\varphi \rightarrow \psi) \vee (\neg \varphi \vee \psi)) \vee \neg (\neg (\neg \varphi \vee \psi) \vee (\varphi \rightarrow \psi))) \)
mpbi l0 _