Theorem elimge0

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

	Ref	Expression
Assertion	elimge0	⊢ 0 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝐴 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → ( 0 ≤ 𝐴 ↔ 0 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
2		breq2	⊢ ( 0 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
3		0re	⊢ 0 ∈ ℝ
4	3	leidi	⊢ 0 ≤ 0
5	1 2 4	elimhyp	⊢ 0 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 )