Metamath Proof Explorer

Theorem truimfal

Description: A -> identity. (Contributed by Anthony Hart, 22-Oct-2010) (Proof shortened by Andrew Salmon, 13-May-2011)

Ref Expression
Assertion truimfal ⊢ ⊤ → ⊥ ↔ ⊥

Proof

Step Hyp Ref Expression
1 trut ⊢ ⊥ ↔ ⊤ → ⊥
2 1 bicomi ⊢ ⊤ → ⊥ ↔ ⊥