Theorem neeq1d 2358

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 2353	. 2 |- ( A = B -> ( A =/= C <-> B =/= C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   =/= wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341

This theorem is referenced by:  neeq12d  2360  eqnetrd  2364  prnzg  3705  hashprg  10730  algcvg  11989  algcvga  11992  eucalgcvga  11999  rpdvds  12040  phibndlem  12157  dfphi2  12161  pcaddlem  12279  ennnfoneleminc  12353  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemnn0  12364  ennnfonelemr  12365  ennnfonelemim  12366  ctinfomlemom  12369  lgsne0  13654  dceqnconst  14013  dcapnconst  14014  nconstwlpolem  14018