Theorem neeq2d 2681

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1405   =/= wne 2598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-cleq 2394  df-ne 2600

This theorem is referenced by:  neeq12dOLD  2683  neeq2  2686  neeqtrd  2698  fndifnfp  6079  f12dfv  6159  f13dfv  6160  infpssrlem4  8717  sqrt2irr  14189  dsmmval  19061  dsmmbas2  19064  frlmbas  19082  frlmbasOLD  19083  dfcon2  20210  alexsublem  20834  uc1pval  22830  mon1pval  22832  dchrsum2  23922  iscgra  24552  usgrcyclnl1  25044  numclwwlkovq  25503  eigorth  27156  eighmorth  27282  wlimeq12  30062  nofulllem5  30153  limsucncmpi  30664  pridlval  31692  maxidlval  31698  lshpset  31976  lduallkr3  32160  isatl  32297  cdlemk42  33940  stoweidlem43  37174