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

Theorem eqnetrd 2465
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetrd.1  |-  ( ph  ->  A  =  B )
eqnetrd.2  |-  ( ph  ->  B  =/=  C )
Assertion
Ref Expression
eqnetrd  |-  ( ph  ->  A  =/=  C )

Proof of Theorem eqnetrd
StepHypRef Expression
1 eqnetrd.2 . 2  |-  ( ph  ->  B  =/=  C )
2 eqnetrd.1 . . 3  |-  ( ph  ->  A  =  B )
32neeq1d 2460 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
41, 3mpbird 223 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    =/= wne 2447
This theorem is referenced by:  eqnetrrd  2467  opnz  4241  frsn  4759  onoviun  6356  intrnfi  7166  cantnfp1lem2  7377  cantnfp1lem3  7378  wemapwe  7396  acndom2  7677  fin23lem14  7955  fin23lem40  7973  isf32lem6  7980  isf34lem5  8000  isf34lem7  8001  isf34lem6  8002  axcc2lem  8058  xaddnemnf  10557  xaddnepnf  10558  fseqsupcl  11035  hashprg  11364  limsupgre  11951  isercolllem3  12136  tanval3  12410  tanneg  12424  ruclem11  12514  phibndlem  12834  dfphi2  12838  0ram  13063  0ram2  13064  ram0  13065  0ramcl  13066  gsumval2  14456  issubg2  14632  ghmrn  14692  gsumval3  15187  pgpfaclem2  15313  ablfaclem2  15317  ablfaclem3  15318  abvdom  15599  lbsextlem2  15908  gzrngunit  16433  zrngunit  16434  iinopn  16644  cnconn  17144  1stcfb  17167  fbasrn  17575  fclscmpi  17720  alexsublem  17734  dscmet  18091  reperflem  18319  evth  18453  cmetcaulem  18710  iscmet3  18715  cmetss  18736  bcthlem5  18746  bcth2  18748  mbflimsup  19017  itg1addlem4  19050  itg1climres  19065  itg2monolem1  19101  itg2i1fseq2  19107  tdeglem4  19442  deg1add  19485  deg1mul2  19496  deg1tm  19500  dgreq  19622  dgradd2  19645  dgrmul  19647  dgrmulc  19648  dgrcolem1  19650  plyrem  19681  facth  19682  fta1lem  19683  vieta1lem1  19686  vieta1lem2  19687  vieta1  19688  qaa  19699  aareccl  19702  geolim3  19715  aaliou3lem9  19726  coseq00topi  19866  cosne0  19888  tanord  19896  tanarg  19966  cxpne0  20020  cxpsqr  20046  chordthmlem  20125  chordthmlem2  20126  dcubic  20138  mcubic  20139  cubic2  20140  cubic  20141  quartlem4  20152  atandmneg  20198  atandmcj  20201  atancj  20202  atanrecl  20203  atanlogsublem  20207  efiatan2  20209  tanatan  20211  atandmtan  20212  cosatan  20213  cosatanne0  20214  wilthlem2  20303  ftalem7  20312  basellem2  20315  basellem4  20317  basellem5  20318  isppw  20348  dchrptlem2  20500  lgsne0  20568  2sqlem8a  20606  2sqlem8  20607  derangenlem  23109  subfacp1lem3  23120  subfacp1lem5  23122  ivthALT  25669  neibastop1  25719  cmpfiiin  26183  pell1234qrne0  26349  rmxyneg  26416  bezoutr1  26484  fnwe2lem2  26559  kelac1  26572  frlmssuvc2  26658  pmtrmvd  26809  cnmsgnsubg  26845  stoweidlem23  27183  stoweidlem31  27191  wallispilem4  27228  wallispi  27230  stirlinglem3  27236  stirlinglem14  27247  logccne0ALT  27537  lsatfixedN  28478  islshpat  28486  lkrshp  28574  2llnm3N  29037  dalemdnee  29134  cdleme18b  29760  cdleme40m  29935  cdlemg12g  30117  cdlemh  30285  cdlemj3  30291  tendoconid  30297  cdlemk3  30301  cdlemk12  30318  cdlemk12u  30340  cdlemk46  30416  cdlemk54  30426  erngdvlem4  30459  erngdvlem4-rN  30467  dibn0  30622  dihglblem2aN  30762  dochshpncl  30853  dochsnnz  30919  dochsatshpb  30921  lcfl7lem  30968  lcfl8b  30973  lcfrlem33  31044  lcfr  31054  hdmaprnlem3uN  31323
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 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-cleq 2277  df-ne 2449
  Copyright terms: Public domain W3C validator