Theorem neeq2d 2620

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)

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	. 2 |- ( ph -> A = B )
2		neeq2 2615	. 2 |- ( A = B -> ( C =/= A <-> C =/= B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1364   =/= wne 2604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434  df-ne 2606

This theorem is referenced by:  neeq12d  2621  neeqtrd  2628  fndifnfp  5904  infpssrlem4  8471  sqr2irr  13527  dsmmval  18059  dsmmbas2  18062  frlmbas  18080  frlmbasOLD  18081  dfcon2  18923  alexsublem  19516  uc1pval  21554  mon1pval  21556  dchrsum2  22550  usgrcyclnl1  23445  eigorth  25161  eighmorth  25287  wlimeq12  27669  nofulllem5  27760  limsucncmpi  28205  pridlval  28742  maxidlval  28748  stoweidlem43  29747  f12dfv  30055  f13dfv  30056  numclwwlkovq  30601  lshpset  32311  lduallkr3  32495  isatl  32632  cdlemk42  34273