Theorem neeq1d 2327

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 2322	. 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 1332   =/= wne 2309

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 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-ne 2310

This theorem is referenced by:  neeq12d  2329  eqnetrd  2333  prnzg  3655  hashprg  10586  algcvg  11765  algcvga  11768  eucalgcvga  11775  rpdvds  11816  phibndlem  11928  dfphi2  11932  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemnn0  11971  ennnfonelemr  11972  ennnfonelemim  11973  ctinfomlemom  11976  dceqnconst  13423