Metamath Proof Explorer


Theorem fald

Description: Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018)

Ref Expression
Assertion fald ( 𝜃 → ¬ ⊥ )

Proof

Step Hyp Ref Expression
1 fal ¬ ⊥
2 1 a1i ( 𝜃 → ¬ ⊥ )