Theorem nexntru

Description: There does not exist a set such that T. is not true. (Contributed by Anthony Hart, 13-Sep-2011)

	Ref	Expression
Assertion	nexntru	$$⊢\neg \exists x\neg \top$$

Proof

Step	Hyp	Ref	Expression
1		tru	$$⊢\top$$
2	1	notnoti	$$⊢\neg \neg \top$$
3	2	nex	$$⊢\neg \exists x\neg \top$$