Theorem neeq2d 2698

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
neeq2d	|- ( ph -> ( C =/= A <-> C =/= B ) )

Proof of Theorem neeq2d

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 |- ( ph -> A = B )
2	1	eqeq2d 2436	. 2 |- ( ph -> ( C = A <-> C = B ) )
3	2	necon3bid 2678	1 |- ( ph -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   =/= wne 2614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2616

This theorem is referenced by:  neeq12dOLD  2700  neeq2  2703  neeqtrd  2715  fndifnfp  6108  f12dfv  6187  f13dfv  6188  infpssrlem4  8743  sqrt2irr  14300  dsmmval  19295  dsmmbas2  19298  frlmbas  19316  dfcon2  20432  alexsublem  21057  uc1pval  23088  mon1pval  23090  dchrsum2  24194  isinag  24877  usgrcyclnl1  25366  numclwwlkovq  25825  eigorth  27489  eighmorth  27615  wlimeq12  30509  nofulllem5  30600  limsucncmpi  31110  poimirlem25  31929  poimirlem26  31930  pridlval  32230  maxidlval  32236  lshpset  32513  lduallkr3  32697  isatl  32834  cdlemk42  34477  stoweidlem43  37844  nnfoctbdjlem  38201