MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq2d Structured version   Unicode version

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
StepHypRef Expression
1 neeq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21eqeq2d 2436 . 2  |-  ( ph  ->  ( C  =  A  <-> 
C  =  B ) )
32necon3bid 2678 1  |-  ( ph  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator