Theorem neeq1d 2396

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 2391	. 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 1373   =/= wne 2378

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-ne 2379

This theorem is referenced by:  neeq12d  2398  eqnetrd  2402  prnzg  3768  pw2f1odclem  6956  hashprg  10990  algcvg  12485  algcvga  12488  eucalgcvga  12495  rpdvds  12536  phibndlem  12653  dfphi2  12657  pcaddlem  12777  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemnn0  12908  ennnfonelemr  12909  ennnfonelemim  12910  ctinfomlemom  12913  setscomd  12988  lgsne0  15630  dceqnconst  16201  dcapnconst  16202  nconstwlpolem  16206