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 θ ¬