Theorem neeq1d 2430

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 2425	. 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 1398   =/= wne 2412

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  neeq12d  2432  eqnetrd  2436  prnzg  3817  suppval1  6439  elsuppfng  6442  elsuppfn  6443  suppsnopdc  6450  ressuppss  6454  pw2f1odclem  7087  hashprg  11173  algcvg  12745  algcvga  12748  eucalgcvga  12755  rpdvds  12796  phibndlem  12913  dfphi2  12917  pcaddlem  13037  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemnn0  13173  ennnfonelemr  13174  ennnfonelemim  13175  ctinfomlemom  13178  setscomd  13253  rrgsupp  14411  pellexlem3  15847  lgsne0  15911  umgr2cwwkdifex  16420  dceqnconst  16846  dcapnconst  16847  nconstwlpolem  16851