Metamath Proof Explorer

Theorem noror

Description: \/ is expressible via -\/ . (Contributed by Remi, 26-Oct-2023) (Proof shortened by Wolf Lammen, 8-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 df-nor ⊢ φ ⊽ ψ ↔ ¬ φ ∨ ψ
2 1 con2bii ⊢ φ ∨ ψ ↔ ¬ φ ⊽ ψ
3 nornot ⊢ ¬ φ ⊽ ψ ↔ φ ⊽ ψ ⊽ φ ⊽ ψ
4 2 3 bitri ⊢ φ ∨ ψ ↔ φ ⊽ ψ ⊽ φ ⊽ ψ