Metamath Proof Explorer


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