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

Theorem neeq2d 2460
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
StepHypRef Expression
1 neeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 neeq2 2455 . 2  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  neeq12d  2461  neeqtrd  2468  infpssrlem4  7932  sqr2irr  12527  dfcon2  17145  alexsublem  17738  uc1pval  19525  mon1pval  19527  dchrsum2  20507  eigorth  22418  eighmorth  22544  disjdsct  23369  nofulllem5  24360  limsucncmpi  24884  pridlval  26658  maxidlval  26664  fndifnfp  26756  dsmmval  27200  dsmmbas2  27203  frlmbas  27223  stoweidlem43  27792  lshpset  29168  lduallkr3  29352  isatl  29489  cdlemk42  31130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator