Theorem neeq1d 2393

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 2388	. 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 1372   =/= wne 2375

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-ne 2376

This theorem is referenced by:  neeq12d  2395  eqnetrd  2399  prnzg  3756  pw2f1odclem  6930  hashprg  10951  algcvg  12341  algcvga  12344  eucalgcvga  12351  rpdvds  12392  phibndlem  12509  dfphi2  12513  pcaddlem  12633  ennnfoneleminc  12753  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemnn0  12764  ennnfonelemr  12765  ennnfonelemim  12766  ctinfomlemom  12769  setscomd  12844  lgsne0  15486  dceqnconst  15961  dcapnconst  15962  nconstwlpolem  15966