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

Theorem neeq1d 2472
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 2467 . 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 1632    =/= wne 2459
This theorem is referenced by:  neeq12d  2474  eqnetrd  2477  prnzg  3759  tz7.49  6473  ereldm  6719  pw2f1olem  6982  marypha1lem  7202  wdomtr  7305  inf3lem2  7346  cantnf  7411  cplem2  7576  dfac9  7778  kmlem12  7803  infpssrlem4  7948  fin23lem14  7975  axcc2lem  8078  axcc3  8080  domtriomlem  8084  axdc2lem  8090  ac6c4  8124  zorn2lem6  8144  rpnnen1lem4  10361  rpnnen1lem5  10362  hashprg  11384  dvdsle  12590  algcvg  12762  algcvga  12765  eucalgcvga  12772  rpdvds  12819  phibndlem  12854  dfphi2  12858  pcaddlem  12952  vdwmc  13041  iscatd2  13599  frgpup3lem  15102  isirred  15497  isdrngrd  15554  elcls  16826  clsndisj  16828  elcls3  16836  neindisj2  16876  clslp  16895  cmpfi  17151  cmpfii  17152  dfcon2  17161  consuba  17162  nconsubb  17165  1stcelcls  17203  ptclsg  17325  dfac14lem  17327  isfbas  17540  trfbas2  17554  isfil  17558  filss  17564  fbunfip  17580  fgval  17581  elfg  17582  isufil2  17619  ufileu  17630  filufint  17631  fmfnfm  17669  flimclslem  17695  fclsopni  17726  fclsnei  17730  fclsbas  17732  fclsrest  17735  fclscmp  17741  ufilcmp  17743  isfcf  17745  fcfnei  17746  fcfneii  17748  ptcmplem2  17763  tsmsfbas  17826  lpbl  18065  prdsxmslem2  18091  qdensere  18295  lebnumlem3  18477  isphtpc  18508  iscmet  18726  cmetcvg  18727  equivcmet  18757  ovolicc2lem2  18893  ovolicc2lem5  18896  i1fres  19076  lhop1lem  19376  deg1ldg  19494  plyco0  19590  plyeq0lem  19608  coeeq2  19640  coe1termlem  19655  taylfval  19754  cxpeq0  20041  ftalem4  20329  ftalem5  20330  ftalem6  20331  isppw  20368  isnsqf  20389  sqff1o  20436  musum  20447  dchrelbas3  20493  dchrelbasd  20494  dchrelbas4  20498  dchrmulcl  20504  dchrn0  20505  dchrfi  20510  dchrptlem2  20520  dchrpt  20522  lgsne0  20588  lgsdchr  20603  2sqlem11  20630  nmorepnf  21362  nmoprepnf  22463  nmfnrepnf  22476  disjdsct  23384  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  subfacp1  23732  iscvm  23805  cvmcov  23809  cvmcov2  23821  eldm3  24190  nobndlem2  24418  nobndlem4  24420  nobndlem5  24421  nobndlem6  24422  nobndlem8  24424  nobndup  24425  nobnddown  24426  nofulllem5  24431  itg2addnc  25005  cnfilca  25659  isconcl2b  26201  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  isibg2aalem3  26218  lppotos  26247  nbssntrs  26250  pdiveql  26271  finlocfin  26402  locfincmp  26407  locfindis  26408  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  neibastop3  26414  neifg  26423  sstotbnd2  26601  cntotbnd  26623  heibor1lem  26636  pellexlem3  27019  inisegn0  27243  dsmmelbas  27308  dsmmacl  27310  frlmssuvc2  27350  mncn0  27447  aaitgo  27470  pmtrmvd  27501  stoweidlem43  27895  stoweidlem59  27911  hashtpg  28217  uvtx01vtx  28305  secval  28471  cscval  28472  cotval  28473  2llnm3N  30380  dalem4  30476  cdlemk28-3  31719  mapdh9a  32602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator