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 ⊢ φ ↔ ψ ↔ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ