Theorem elimge0

Description: Hypothesis for weak deduction theorem to eliminate 0 <_ A . (Contributed by NM, 30-Jul-1999)

	Ref	Expression
Assertion	elimge0	$$⊢0\le if\left(0\le A,A,0\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢A=if\left(0\le A,A,0\right)\to \left(0\le A\leftrightarrow 0\le if\left(0\le A,A,0\right)\right)$$
2		breq2	$$⊢0=if\left(0\le A,A,0\right)\to \left(0\le 0\leftrightarrow 0\le if\left(0\le A,A,0\right)\right)$$
3		0re	$$⊢0\in ℝ$$
4	3	leidi	$$⊢0\le 0$$
5	1 2 4	elimhyp	$$⊢0\le if\left(0\le A,A,0\right)$$