Theorem neeq1d 2438

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)

Hypothesis

Ref	Expression
neeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
neeq1d	|- ( ph -> ( A =/= C <-> B =/= C ) )

Proof of Theorem neeq1d

Step	Hyp	Ref	Expression
1		neeq1d.1	. 2 |- ( ph -> A = B )
2		neeq1 2433	. 2 |- ( A = B -> ( A =/= C <-> B =/= C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   =/= wne 2420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  neeq12d  2440  eqnetrd  2444  prnzg  3833  suppval1  6469  elsuppfng  6472  elsuppfn  6473  suppsnopdc  6480  ressuppss  6484  pw2f1odclem  7124  hashprg  11227  algcvg  12804  algcvga  12807  eucalgcvga  12814  rpdvds  12855  phibndlem  12972  dfphi2  12976  pcaddlem  13096  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemnn0  13291  ennnfonelemr  13292  ennnfonelemim  13293  ctinfomlemom  13296  setscomd  13371  rrgsupp  14547  pellexlem3  16007  lgsne0  16071  umgr2cwwkdifex  16580  dceqnconst  17015  dcapnconst  17016  nconstwlpolem  17020