Theorem neeq1d 2326

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 2321	. 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 1331   =/= wne 2308

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 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-ne 2309

This theorem is referenced by:  neeq12d  2328  eqnetrd  2332  prnzg  3647  hashprg  10554  algcvg  11729  algcvga  11732  eucalgcvga  11739  rpdvds  11780  phibndlem  11892  dfphi2  11896  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemnn0  11935  ennnfonelemr  11936  ennnfonelemim  11937  ctinfomlemom  11940