Theorem elimgt0

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

	Ref	Expression
Assertion	elimgt0	$$⊢0<if\left(0<A,A,1\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢A=if\left(0<A,A,1\right)\to \left(0<A\leftrightarrow 0<if\left(0<A,A,1\right)\right)$$
2		breq2	$$⊢1=if\left(0<A,A,1\right)\to \left(0<1\leftrightarrow 0<if\left(0<A,A,1\right)\right)$$
3		0lt1	$$⊢0<1$$
4	1 2 3	elimhyp	$$⊢0<if\left(0<A,A,1\right)$$