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

Theorem neeq2d 2617
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 2612 . 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 178    = wceq 1653    =/= wne 2601
This theorem is referenced by:  neeq12d  2618  neeqtrd  2625  infpssrlem4  8191  sqr2irr  12853  dfcon2  17487  alexsublem  18080  uc1pval  20067  mon1pval  20069  dchrsum2  21057  usgrcyclnl1  21632  eigorth  23346  eighmorth  23472  disjdsct  24095  wlimeq12  25575  nofulllem5  25666  limsucncmpi  26200  pridlval  26657  maxidlval  26663  fndifnfp  26751  dsmmval  27191  dsmmbas2  27194  frlmbas  27214  stoweidlem43  27782  f12dfv  28098  f13dfv  28099  lshpset  29850  lduallkr3  30034  isatl  30171  cdlemk42  31812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator