Theorem neeq2d 2730

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 2468	. 2 |- ( ph -> ( C = A <-> C = B ) )
3	2	necon3bid 2710	1 |- ( ph -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   =/= wne 2648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2650

This theorem is referenced by:  neeq12dOLD  2732  neeq2  2735  neeqtrd  2747  fndifnfp  6019  infpssrlem4  8590  sqr2irr  13653  dsmmval  18294  dsmmbas2  18297  frlmbas  18315  frlmbasOLD  18316  dfcon2  19165  alexsublem  19758  uc1pval  21754  mon1pval  21756  dchrsum2  22750  usgrcyclnl1  23705  eigorth  25421  eighmorth  25547  wlimeq12  27923  nofulllem5  28014  limsucncmpi  28458  pridlval  29004  maxidlval  29010  stoweidlem43  30009  f12dfv  30317  f13dfv  30318  numclwwlkovq  30863  lshpset  32986  lduallkr3  33170  isatl  33307  cdlemk42  34948