Metamath Proof Explorer


Theorem rpgecld

Description: A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpgecld.1 φA
rpgecld.2 φB+
rpgecld.3 φBA
Assertion rpgecld φA+

Proof

Step Hyp Ref Expression
1 rpgecld.1 φA
2 rpgecld.2 φB+
3 rpgecld.3 φBA
4 rpgecl B+ABAA+
5 2 1 3 4 syl3anc φA+