Theorem trunorfal

Description: A -\/ identity. (Contributed by Remi, 25-Oct-2023) (Proof shortened by Wolf Lammen, 17-Dec-2023)

	Ref	Expression
Assertion	trunorfal	⊢ ( ( ⊤ ⊽ ⊥ ) ↔ ⊥ )

Proof

Step	Hyp	Ref	Expression
1		df-nor	⊢ ( ( ⊤ ⊽ ⊥ ) ↔ ¬ ( ⊤ ∨ ⊥ ) )
2		truorfal	⊢ ( ( ⊤ ∨ ⊥ ) ↔ ⊤ )
3	1 2	xchbinx	⊢ ( ( ⊤ ⊽ ⊥ ) ↔ ¬ ⊤ )
4		df-fal	⊢ ( ⊥ ↔ ¬ ⊤ )
5	3 4	bitr4i	⊢ ( ( ⊤ ⊽ ⊥ ) ↔ ⊥ )