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

Theorem neeq1d 2580
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 2575 . 2  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    =/= wne 2567
This theorem is referenced by:  neeq12d  2582  eqnetrd  2585  prnzg  3884  tz7.49  6661  ereldm  6907  pw2f1olem  7171  marypha1lem  7396  wdomtr  7499  inf3lem2  7540  cantnf  7605  cplem2  7770  dfac9  7972  kmlem12  7997  infpssrlem4  8142  fin23lem14  8169  axcc2lem  8272  axcc3  8274  domtriomlem  8278  axdc2lem  8284  ac6c4  8317  zorn2lem6  8337  rpnnen1lem4  10559  rpnnen1lem5  10560  hashprg  11621  hashtpg  11646  dvdsle  12850  algcvg  13022  algcvga  13025  eucalgcvga  13032  rpdvds  13079  phibndlem  13114  dfphi2  13118  pcaddlem  13212  vdwmc  13301  iscatd2  13861  frgpup3lem  15364  isirred  15759  isdrngrd  15816  elcls  17092  clsndisj  17094  elcls3  17102  neindisj2  17142  clslp  17166  cmpfi  17425  cmpfii  17426  dfcon2  17435  consuba  17436  nconsubb  17439  1stcelcls  17477  ptclsg  17600  dfac14lem  17602  isfbas  17814  trfbas2  17828  isfil  17832  filss  17838  fbunfip  17854  fgval  17855  elfg  17856  isufil2  17893  ufileu  17904  filufint  17905  fmfnfm  17943  flimclslem  17969  fclsopni  18000  fclsnei  18004  fclsbas  18006  fclsrest  18009  fclscmp  18015  ufilcmp  18017  isfcf  18019  fcfnei  18020  fcfneii  18022  ptcmplem2  18037  cnextcn  18051  cnextfres  18052  tsmsfbas  18110  iscusp  18282  cuspcvg  18284  lpbl  18486  prdsxmslem2  18512  restmetu  18570  qdensere  18757  lebnumlem3  18941  isphtpc  18972  iscmet  19190  cmetcvg  19191  equivcmet  19221  cmetcusp1OLD  19258  cmetcusp1  19259  cmetcuspOLD  19260  cmetcusp  19261  ovolicc2lem2  19367  ovolicc2lem5  19370  i1fres  19550  lhop1lem  19850  deg1ldg  19968  plyco0  20064  plyeq0lem  20082  coeeq2  20114  coe1termlem  20129  taylfval  20228  cxpeq0  20522  ftalem4  20811  ftalem5  20812  ftalem6  20813  isppw  20850  isnsqf  20871  sqff1o  20918  musum  20929  dchrelbas3  20975  dchrelbasd  20976  dchrelbas4  20980  dchrmulcl  20986  dchrn0  20987  dchrfi  20992  dchrptlem2  21002  dchrpt  21004  lgsne0  21070  lgsdchr  21085  2sqlem11  21112  uvtx01vtx  21454  nmorepnf  22222  nmoprepnf  23323  nmfnrepnf  23336  disjdsct  24043  sibfof  24607  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  subfacp1  24825  iscvm  24899  cvmcov  24903  cvmcov2  24915  prodfn0  25175  prodfrec  25176  prodfdiv  25177  ntrivcvgtail  25181  fproddiv  25238  fprodn0  25256  eldm3  25333  nobndlem2  25561  nobndlem4  25563  nobndlem5  25564  nobndlem6  25565  nobndlem8  25567  nobndup  25568  nobnddown  25569  nofulllem5  25574  mblfinlem2  26144  itg2addnclem3  26157  finlocfin  26269  locfincmp  26274  locfindis  26275  neibastop1  26278  neibastop2lem  26279  neibastop2  26280  neibastop3  26281  neifg  26290  sstotbnd2  26373  cntotbnd  26395  heibor1lem  26408  pellexlem3  26784  inisegn0  27008  dsmmelbas  27073  dsmmacl  27075  frlmssuvc2  27115  mncn0  27212  aaitgo  27235  pmtrmvd  27266  stoweidlem28  27644  stoweidlem43  27659  f12dfv  27961  f13dfv  27962  frgraregorufr  28156  secval  28204  cscval  28205  cotval  28206  2llnm3N  30051  dalem4  30147  cdlemk28-3  31390  mapdh9a  32273
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