Metamath Proof Explorer

Theorem noranOLD

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

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

Proof

Step Hyp Ref Expression
1 ianor ⊢ ¬ φ ∧ ψ ↔ ¬ φ ∨ ¬ ψ
2 1 notbii ⊢ ¬ ¬ φ ∧ ψ ↔ ¬ ¬ φ ∨ ¬ ψ
3 nornot ⊢ ¬ φ ↔ φ ⊽ φ
4 nornot ⊢ ¬ ψ ↔ ψ ⊽ ψ
5 3 4 orbi12i ⊢ ¬ φ ∨ ¬ ψ ↔ φ ⊽ φ ∨ ψ ⊽ ψ
6 5 notbii ⊢ ¬ ¬ φ ∨ ¬ ψ ↔ ¬ φ ⊽ φ ∨ ψ ⊽ ψ
7 ioran ⊢ ¬ φ ⊽ φ ∨ ψ ⊽ ψ ↔ ¬ φ ⊽ φ ∧ ¬ ψ ⊽ ψ
8 2 6 7 3bitrri ⊢ ¬ φ ⊽ φ ∧ ¬ ψ ⊽ ψ ↔ ¬ ¬ φ ∧ ψ
9 df-nor ⊢ φ ⊽ φ ⊽ ψ ⊽ ψ ↔ ¬ φ ⊽ φ ∨ ψ ⊽ ψ
10 9 7 bitri ⊢ φ ⊽ φ ⊽ ψ ⊽ ψ ↔ ¬ φ ⊽ φ ∧ ¬ ψ ⊽ ψ
11 notnotb ⊢ φ ∧ ψ ↔ ¬ ¬ φ ∧ ψ
12 8 10 11 3bitr4ri ⊢ φ ∧ ψ ↔ φ ⊽ φ ⊽ ψ ⊽ ψ