Metamath Proof Explorer

Theorem elimgt0

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

Ref Expression
Assertion elimgt0 
|- 0 < if ( 0 < A , A , 1 )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( A = if ( 0 < A , A , 1 ) -> ( 0 < A <-> 0 < if ( 0 < A , A , 1 ) ) )
2 breq2 
 |-  ( 1 = if ( 0 < A , A , 1 ) -> ( 0 < 1 <-> 0 < if ( 0 < A , A , 1 ) ) )
3 0lt1 
 |-  0 < 1
4 1 2 3 elimhyp 
 |-  0 < if ( 0 < A , A , 1 )