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

Theorem neeq1d 2459
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
Hypothesis
Ref Expression
neeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
neeq1d  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )

Proof of Theorem neeq1d
StepHypRef Expression
1 neeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 neeq1 2454 . 2  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2syl 15 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  neeq12d  2461  eqnetrd  2464  prnzg  3746  tz7.49  6457  ereldm  6703  pw2f1olem  6966  marypha1lem  7186  wdomtr  7289  inf3lem2  7330  cantnf  7395  cplem2  7560  dfac9  7762  kmlem12  7787  infpssrlem4  7932  fin23lem14  7959  axcc2lem  8062  axcc3  8064  domtriomlem  8068  axdc2lem  8074  ac6c4  8108  zorn2lem6  8128  rpnnen1lem4  10345  rpnnen1lem5  10346  hashprg  11368  dvdsle  12574  algcvg  12746  algcvga  12749  eucalgcvga  12756  rpdvds  12803  phibndlem  12838  dfphi2  12842  pcaddlem  12936  vdwmc  13025  iscatd2  13583  frgpup3lem  15086  isirred  15481  isdrngrd  15538  elcls  16810  clsndisj  16812  elcls3  16820  neindisj2  16860  clslp  16879  cmpfi  17135  cmpfii  17136  dfcon2  17145  consuba  17146  nconsubb  17149  1stcelcls  17187  ptclsg  17309  dfac14lem  17311  isfbas  17524  trfbas2  17538  isfil  17542  filss  17548  fbunfip  17564  fgval  17565  elfg  17566  isufil2  17603  ufileu  17614  filufint  17615  fmfnfm  17653  flimclslem  17679  fclsopni  17710  fclsnei  17714  fclsbas  17716  fclsrest  17719  fclscmp  17725  ufilcmp  17727  isfcf  17729  fcfnei  17730  fcfneii  17732  ptcmplem2  17747  tsmsfbas  17810  lpbl  18049  prdsxmslem2  18075  qdensere  18279  lebnumlem3  18461  isphtpc  18492  iscmet  18710  cmetcvg  18711  equivcmet  18741  ovolicc2lem2  18877  ovolicc2lem5  18880  i1fres  19060  lhop1lem  19360  deg1ldg  19478  plyco0  19574  plyeq0lem  19592  coeeq2  19624  coe1termlem  19639  taylfval  19738  cxpeq0  20025  ftalem4  20313  ftalem5  20314  ftalem6  20315  isppw  20352  isnsqf  20373  sqff1o  20420  musum  20431  dchrelbas3  20477  dchrelbasd  20478  dchrelbas4  20482  dchrmulcl  20488  dchrn0  20489  dchrfi  20494  dchrptlem2  20504  dchrpt  20506  lgsne0  20572  lgsdchr  20587  2sqlem11  20614  nmorepnf  21346  nmoprepnf  22447  nmfnrepnf  22460  disjdsct  23369  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  subfacp1  23717  iscvm  23790  cvmcov  23794  cvmcov2  23806  eldm3  24119  nobndlem2  24347  nobndlem4  24349  nobndlem5  24350  nobndlem6  24351  nobndlem8  24353  nobndup  24354  nobnddown  24355  nofulllem5  24360  cnfilca  25556  isconcl2b  26098  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  isibg2aalem3  26115  lppotos  26144  nbssntrs  26147  pdiveql  26168  finlocfin  26299  locfincmp  26304  locfindis  26305  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  neifg  26320  sstotbnd2  26498  cntotbnd  26520  heibor1lem  26533  pellexlem3  26916  inisegn0  27140  dsmmelbas  27205  dsmmacl  27207  frlmssuvc2  27247  mncn0  27344  aaitgo  27367  pmtrmvd  27398  stoweidlem43  27792  stoweidlem59  27808  uvtx01vtx  28164  secval  28217  cscval  28218  cotval  28219  2llnm3N  29758  dalem4  29854  cdlemk28-3  31097  mapdh9a  31980
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