Metamath Proof Explorer


Theorem rb-bijust

Description: Justification for rb-imdf . (Contributed by Anthony Hart, 17-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rb-bijust ( ( 𝜑𝜓 ) ↔ ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 dfbi1 ( ( 𝜑𝜓 ) ↔ ¬ ( ( 𝜑𝜓 ) → ¬ ( 𝜓𝜑 ) ) )
2 imor ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜓 ) )
3 imor ( ( 𝜓𝜑 ) ↔ ( ¬ 𝜓𝜑 ) )
4 3 notbii ( ¬ ( 𝜓𝜑 ) ↔ ¬ ( ¬ 𝜓𝜑 ) )
5 2 4 imbi12i ( ( ( 𝜑𝜓 ) → ¬ ( 𝜓𝜑 ) ) ↔ ( ( ¬ 𝜑𝜓 ) → ¬ ( ¬ 𝜓𝜑 ) ) )
6 5 notbii ( ¬ ( ( 𝜑𝜓 ) → ¬ ( 𝜓𝜑 ) ) ↔ ¬ ( ( ¬ 𝜑𝜓 ) → ¬ ( ¬ 𝜓𝜑 ) ) )
7 pm4.62 ( ( ( ¬ 𝜑𝜓 ) → ¬ ( ¬ 𝜓𝜑 ) ) ↔ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) )
8 7 notbii ( ¬ ( ( ¬ 𝜑𝜓 ) → ¬ ( ¬ 𝜓𝜑 ) ) ↔ ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) )
9 1 6 8 3bitri ( ( 𝜑𝜓 ) ↔ ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) )