Theorem trunortru

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

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

Proof

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