Theorem elimne0

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

	Ref	Expression
Assertion	elimne0	$$⊢if\left(A\ne 0,A,1\right)\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		neeq1	$$⊢A=if\left(A\ne 0,A,1\right)\to \left(A\ne 0\leftrightarrow if\left(A\ne 0,A,1\right)\ne 0\right)$$
2		neeq1	$$⊢1=if\left(A\ne 0,A,1\right)\to \left(1\ne 0\leftrightarrow if\left(A\ne 0,A,1\right)\ne 0\right)$$
3		ax-1ne0	$$⊢1\ne 0$$
4	1 2 3	elimhyp	$$⊢if\left(A\ne 0,A,1\right)\ne 0$$