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

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