Metamath Proof Explorer


Theorem 0npr

Description: The empty set is not a positive real. (Contributed by NM, 15-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion 0npr ¬ 𝑷

Proof

Step Hyp Ref Expression
1 eqid =
2 prn0 𝑷
3 2 necon2bi = ¬ 𝑷
4 1 3 ax-mp ¬ 𝑷