Metamath Proof Explorer


Theorem aisfina

Description: Given a is equivalent to F. , there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016)

Ref Expression
Hypothesis aisfina.1 φ
Assertion aisfina ¬ φ

Proof

Step Hyp Ref Expression
1 aisfina.1 φ
2 nbfal ¬ φ φ
3 1 2 mpbir ¬ φ