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

Theorem neeq1d 2614
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 2609 . 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 1652    =/= wne 2599
This theorem is referenced by:  neeq12d  2616  eqnetrd  2619  prnzg  3924  tz7.49  6702  ereldm  6948  pw2f1olem  7212  marypha1lem  7438  wdomtr  7543  inf3lem2  7584  cantnf  7649  cplem2  7814  dfac9  8016  kmlem12  8041  infpssrlem4  8186  fin23lem14  8213  axcc2lem  8316  axcc3  8318  domtriomlem  8322  axdc2lem  8328  ac6c4  8361  zorn2lem6  8381  rpnnen1lem4  10603  rpnnen1lem5  10604  hashprg  11666  hashtpg  11691  dvdsle  12895  algcvg  13067  algcvga  13070  eucalgcvga  13077  rpdvds  13124  phibndlem  13159  dfphi2  13163  pcaddlem  13257  vdwmc  13346  iscatd2  13906  frgpup3lem  15409  isirred  15804  isdrngrd  15861  elcls  17137  clsndisj  17139  elcls3  17147  neindisj2  17187  clslp  17212  cmpfi  17471  cmpfii  17472  dfcon2  17482  consuba  17483  nconsubb  17486  1stcelcls  17524  ptclsg  17647  dfac14lem  17649  isfbas  17861  trfbas2  17875  isfil  17879  filss  17885  fbunfip  17901  fgval  17902  elfg  17903  isufil2  17940  ufileu  17951  filufint  17952  fmfnfm  17990  flimclslem  18016  fclsopni  18047  fclsnei  18051  fclsbas  18053  fclsrest  18056  fclscmp  18062  ufilcmp  18064  isfcf  18066  fcfnei  18067  fcfneii  18069  ptcmplem2  18084  cnextcn  18098  cnextfres  18099  tsmsfbas  18157  iscusp  18329  cuspcvg  18331  lpbl  18533  prdsxmslem2  18559  restmetu  18617  qdensere  18804  lebnumlem3  18988  isphtpc  19019  iscmet  19237  cmetcvg  19238  equivcmet  19268  cmetcusp1OLD  19305  cmetcusp1  19306  cmetcuspOLD  19307  cmetcusp  19308  ovolicc2lem2  19414  ovolicc2lem5  19417  i1fres  19597  lhop1lem  19897  deg1ldg  20015  plyco0  20111  plyeq0lem  20129  coeeq2  20161  coe1termlem  20176  taylfval  20275  cxpeq0  20569  ftalem4  20858  ftalem5  20859  ftalem6  20860  isppw  20897  isnsqf  20918  sqff1o  20965  musum  20976  dchrelbas3  21022  dchrelbasd  21023  dchrelbas4  21027  dchrmulcl  21033  dchrn0  21034  dchrfi  21039  dchrptlem2  21049  dchrpt  21051  lgsne0  21117  lgsdchr  21132  2sqlem11  21159  uvtx01vtx  21501  nmorepnf  22269  nmoprepnf  23370  nmfnrepnf  23383  disjdsct  24090  sibfof  24654  derangenlem  24857  subfacp1lem3  24868  subfacp1lem5  24870  subfacp1lem6  24871  subfacp1  24872  iscvm  24946  cvmcov  24950  cvmcov2  24962  prodfn0  25222  prodfrec  25223  prodfdiv  25224  ntrivcvgtail  25228  fproddiv  25285  fprodn0  25303  eldm3  25385  elima4  25404  nobndlem2  25648  nobndlem4  25650  nobndlem5  25651  nobndlem6  25652  nobndlem8  25654  nobndup  25655  nobnddown  25656  nofulllem5  25661  mblfinlem3  26245  itg2addnclem3  26258  finlocfin  26379  locfincmp  26384  locfindis  26385  neibastop1  26388  neibastop2lem  26389  neibastop2  26390  neibastop3  26391  neifg  26400  sstotbnd2  26483  cntotbnd  26505  heibor1lem  26518  pellexlem3  26894  inisegn0  27118  dsmmelbas  27182  dsmmacl  27184  frlmssuvc2  27224  mncn0  27321  aaitgo  27344  pmtrmvd  27375  stoweidlem28  27753  stoweidlem43  27768  f12dfv  28080  f13dfv  28081  cshwssizelem1a  28279  frgraregorufr  28442  secval  28490  cscval  28491  cotval  28492  2llnm3N  30366  dalem4  30462  cdlemk28-3  31705  mapdh9a  32588
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429  df-ne 2601
  Copyright terms: Public domain W3C validator