This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elimne0

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

Ref Expression
Assertion elimne0 ⊢ if A ≠ 0 A 1 ≠ 0

Proof

Step Hyp Ref Expression
1 neeq1 ⊢ A = if A ≠ 0 A 1 → A ≠ 0 ↔ if A ≠ 0 A 1 ≠ 0
2 neeq1 ⊢ 1 = if A ≠ 0 A 1 → 1 ≠ 0 ↔ if A ≠ 0 A 1 ≠ 0
3 ax-1ne0 ⊢ 1 ≠ 0
4 1 2 3 elimhyp ⊢ if A ≠ 0 A 1 ≠ 0