Theorem rb-imdf

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

	Ref	Expression
Assertion	rb-imdf	$$⊢\neg \left(\neg \left(\neg \left(\phi \to \psi \right)\vee \left(\neg \phi \vee \psi \right)\right)\vee \neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \left(\phi \to \psi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imor	$$⊢\left(\phi \to \psi \right)\leftrightarrow \left(\neg \phi \vee \psi \right)$$
2		rb-bijust	$$⊢\left(\left(\phi \to \psi \right)\leftrightarrow \left(\neg \phi \vee \psi \right)\right)\leftrightarrow \neg \left(\neg \left(\neg \left(\phi \to \psi \right)\vee \left(\neg \phi \vee \psi \right)\right)\vee \neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \left(\phi \to \psi \right)\right)\right)$$
3	1 2	mpbi	$$⊢\neg \left(\neg \left(\neg \left(\phi \to \psi \right)\vee \left(\neg \phi \vee \psi \right)\right)\vee \neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \left(\phi \to \psi \right)\right)\right)$$