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	|- ( ph <-> F. )
Assertion	aisfina	|- -. ph

Proof

Step	Hyp	Ref	Expression
1		aisfina.1	|- ( ph <-> F. )
2		nbfal	|- ( -. ph <-> ( ph <-> F. ) )
3	1 2	mpbir	|- -. ph