Theorem neeq1d 2394

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 2389	. 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 2376

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-ne 2377

This theorem is referenced by:  neeq12d  2396  eqnetrd  2400  prnzg  3757  pw2f1odclem  6931  hashprg  10953  algcvg  12370  algcvga  12373  eucalgcvga  12380  rpdvds  12421  phibndlem  12538  dfphi2  12542  pcaddlem  12662  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemnn0  12793  ennnfonelemr  12794  ennnfonelemim  12795  ctinfomlemom  12798  setscomd  12873  lgsne0  15515  dceqnconst  15999  dcapnconst  16000  nconstwlpolem  16004