Metamath Proof Explorer


Theorem fald

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

Ref Expression
Assertion fald
|- ( th -> -. F. )

Proof

Step Hyp Ref Expression
1 fal
 |-  -. F.
2 1 a1i
 |-  ( th -> -. F. )