Metamath Proof Explorer

Theorem nororOLD

Description: Obsolete version of noror as of 8-Dec-2023. (Contributed by Remi, 26-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nororOLD ⊢ φ ∨ ψ ↔ φ ⊽ ψ ⊽ φ ⊽ ψ

Proof

Step Hyp Ref Expression
1 notnotb ⊢ φ ∨ ψ ↔ ¬ ¬ φ ∨ ψ
2 df-nor ⊢ φ ⊽ ψ ↔ ¬ φ ∨ ψ
3 2 notbii ⊢ ¬ φ ⊽ ψ ↔ ¬ ¬ φ ∨ ψ
4 nornot ⊢ ¬ φ ⊽ ψ ↔ φ ⊽ ψ ⊽ φ ⊽ ψ
5 1 3 4 3bitr2ri ⊢ φ ⊽ ψ ⊽ φ ⊽ ψ ↔ φ ∨ ψ
6 5 bicomi ⊢ φ ∨ ψ ↔ φ ⊽ ψ ⊽ φ ⊽ ψ