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

Theorem neeq2d 2535
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 2530 . 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 1642    =/= wne 2521
This theorem is referenced by:  neeq12d  2536  neeqtrd  2543  infpssrlem4  8019  sqr2irr  12618  dfcon2  17245  alexsublem  17834  uc1pval  19623  mon1pval  19625  dchrsum2  20613  eigorth  22526  eighmorth  22652  disjdsct  23291  nofulllem5  24918  limsucncmpi  25443  pridlval  25981  maxidlval  25987  fndifnfp  26079  dsmmval  26523  dsmmbas2  26526  frlmbas  26546  stoweidlem43  27115  usgrcyclnl1  27747  lshpset  29220  lduallkr3  29404  isatl  29541  cdlemk42  31182
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2351  df-ne 2523
  Copyright terms: Public domain W3C validator