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

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