Metamath Proof Explorer

Theorem falantru

Description: A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010)

Ref Expression
Assertion falantru ⊢ ⊥ ∧ ⊤ ↔ ⊥

Proof

Step Hyp Ref Expression
1 fal ⊢ ¬ ⊥
2 1 intnanr ⊢ ¬ ⊥ ∧ ⊤
3 2 bifal ⊢ ⊥ ∧ ⊤ ↔ ⊥