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

Theorem neeq2d 2581
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 2576 . 2  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    =/= wne 2567
This theorem is referenced by:  neeq12d  2582  neeqtrd  2589  infpssrlem4  8142  sqr2irr  12803  dfcon2  17435  alexsublem  18028  uc1pval  20015  mon1pval  20017  dchrsum2  21005  usgrcyclnl1  21580  eigorth  23294  eighmorth  23420  disjdsct  24043  nofulllem5  25574  limsucncmpi  26099  pridlval  26533  maxidlval  26539  fndifnfp  26627  dsmmval  27068  dsmmbas2  27071  frlmbas  27091  stoweidlem43  27659  f12dfv  27961  f13dfv  27962  lshpset  29461  lduallkr3  29645  isatl  29782  cdlemk42  31423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397  df-ne 2569
  Copyright terms: Public domain W3C validator