Theorem neeq1d 2378

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 2373	. 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 1364   =/= wne 2360

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-ne 2361

This theorem is referenced by:  neeq12d  2380  eqnetrd  2384  prnzg  3731  pw2f1odclem  6862  hashprg  10820  algcvg  12080  algcvga  12083  eucalgcvga  12090  rpdvds  12131  phibndlem  12248  dfphi2  12252  pcaddlem  12371  ennnfoneleminc  12462  ennnfonelemex  12465  ennnfonelemhom  12466  ennnfonelemnn0  12473  ennnfonelemr  12474  ennnfonelemim  12475  ctinfomlemom  12478  setscomd  12553  lgsne0  14897  dceqnconst  15267  dcapnconst  15268  nconstwlpolem  15272