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	⊢ ¬ ( ¬ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ∨ ¬ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imor	⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) )
2		rb-bijust	⊢ ( ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) ) ↔ ¬ ( ¬ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ∨ ¬ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜑 → 𝜓 ) ) ) )
3	1 2	mpbi	⊢ ¬ ( ¬ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ∨ ¬ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜑 → 𝜓 ) ) )