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