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