Theorem falnortru

Description: A -\/ identity. (Contributed by Remi, 25-Oct-2023)

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

Proof

Step	Hyp	Ref	Expression
1		norcom	⊢ ( ( ⊥ ⊽ ⊤ ) ↔ ( ⊤ ⊽ ⊥ ) )
2		trunorfal	⊢ ( ( ⊤ ⊽ ⊥ ) ↔ ⊥ )
3	1 2	bitri	⊢ ( ( ⊥ ⊽ ⊤ ) ↔ ⊥ )