Metamath Proof Explorer

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 <_ A , A , 0 )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( A = if ( 0 <_ A , A , 0 ) -> ( 0 <_ A <-> 0 <_ if ( 0 <_ A , A , 0 ) ) )
2 breq2 
 |-  ( 0 = if ( 0 <_ A , A , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( 0 <_ A , A , 0 ) ) )
3 0re 
 |-  0 e. RR
4 3 leidi 
 |-  0 <_ 0
5 1 2 4 elimhyp 
 |-  0 <_ if ( 0 <_ A , A , 0 )