Theorem neeq1d 2385

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 2380	. 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 2367

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  neeq12d  2387  eqnetrd  2391  prnzg  3747  pw2f1odclem  6896  hashprg  10902  algcvg  12226  algcvga  12229  eucalgcvga  12236  rpdvds  12277  phibndlem  12394  dfphi2  12398  pcaddlem  12518  ennnfoneleminc  12638  ennnfonelemex  12641  ennnfonelemhom  12642  ennnfonelemnn0  12649  ennnfonelemr  12650  ennnfonelemim  12651  ctinfomlemom  12654  setscomd  12729  lgsne0  15289  dceqnconst  15714  dcapnconst  15715  nconstwlpolem  15719