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

Theorem neeq2d 2620
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 2615 . 2  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1364    =/= wne 2604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434  df-ne 2606
This theorem is referenced by:  neeq12d  2621  neeqtrd  2628  fndifnfp  5904  infpssrlem4  8471  sqr2irr  13527  dsmmval  18059  dsmmbas2  18062  frlmbas  18080  frlmbasOLD  18081  dfcon2  18923  alexsublem  19516  uc1pval  21554  mon1pval  21556  dchrsum2  22550  usgrcyclnl1  23445  eigorth  25161  eighmorth  25287  wlimeq12  27669  nofulllem5  27760  limsucncmpi  28205  pridlval  28742  maxidlval  28748  stoweidlem43  29747  f12dfv  30055  f13dfv  30056  numclwwlkovq  30601  lshpset  32311  lduallkr3  32495  isatl  32632  cdlemk42  34273
  Copyright terms: Public domain W3C validator