Metamath Proof Explorer

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 ⊢ ⊥ ⊽ ⊤ ↔ ⊥