Metamath Proof Explorer

Theorem noran

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

Ref Expression
Assertion noran ⊢ φ ∧ ψ ↔ φ ⊽ φ ⊽ ψ ⊽ ψ

Proof

Step Hyp Ref Expression
1 anor ⊢ φ ∧ ψ ↔ ¬ ¬ φ ∨ ¬ ψ
2 nornot ⊢ ¬ φ ↔ φ ⊽ φ
3 nornot ⊢ ¬ ψ ↔ ψ ⊽ ψ
4 2 3 orbi12i ⊢ ¬ φ ∨ ¬ ψ ↔ φ ⊽ φ ∨ ψ ⊽ ψ
5 1 4 xchbinx ⊢ φ ∧ ψ ↔ ¬ φ ⊽ φ ∨ ψ ⊽ ψ
6 df-nor ⊢ φ ⊽ φ ⊽ ψ ⊽ ψ ↔ ¬ φ ⊽ φ ∨ ψ ⊽ ψ
7 5 6 bitr4i ⊢ φ ∧ ψ ↔ φ ⊽ φ ⊽ ψ ⊽ ψ