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

Theorem eqnetrd 2568
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 2563 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
41, 3mpbird 224 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    =/= wne 2550
This theorem is referenced by:  eqnetrrd  2570  opnz  4373  frsn  4888  xpimasn  5256  onoviun  6541  intrnfi  7356  cantnfp1lem2  7568  cantnfp1lem3  7569  wemapwe  7587  acndom2  7868  fin23lem14  8146  fin23lem40  8164  isf32lem6  8171  isf34lem5  8191  isf34lem7  8192  isf34lem6  8193  axcc2lem  8249  xaddnemnf  10752  xaddnepnf  10753  fseqsupcl  11243  hashprg  11593  elprchashprn2  11594  limsupgre  12202  isercolllem3  12387  tanval3  12662  tanneg  12676  ruclem11  12766  phibndlem  13086  dfphi2  13090  0ram  13315  0ram2  13316  ram0  13317  0ramcl  13318  gsumval2  14710  issubg2  14886  ghmrn  14946  gsumval3  15441  pgpfaclem2  15567  ablfaclem2  15571  ablfaclem3  15572  abvdom  15853  lbsextlem2  16158  gzrngunit  16687  zrngunit  16688  iinopn  16898  cnconn  17406  1stcfb  17429  fbasrn  17837  fclscmpi  17982  alexsublem  17996  ustuqtop5  18196  cnextucn  18254  dscmet  18491  reperflem  18720  evth  18855  cmetcaulem  19112  iscmet3  19117  cmetss  19138  bcthlem5  19150  bcth2  19152  mbflimsup  19425  itg1addlem4  19458  itg1climres  19473  itg2monolem1  19509  itg2i1fseq2  19515  tdeglem4  19850  deg1add  19893  deg1mul2  19904  deg1tm  19908  dgreq  20030  dgradd2  20053  dgrmul  20055  dgrmulc  20056  dgrcolem1  20058  plyrem  20089  facth  20090  fta1lem  20091  vieta1lem1  20094  vieta1lem2  20095  vieta1  20096  qaa  20107  aareccl  20110  geolim3  20123  aaliou3lem9  20134  coseq00topi  20277  cosne0  20299  tanord  20307  tanarg  20381  cxpne0  20435  cxpsqr  20461  chordthmlem  20540  chordthmlem2  20541  dcubic  20553  mcubic  20554  cubic2  20555  cubic  20556  quartlem4  20567  atandmneg  20613  atandmcj  20616  atancj  20617  atanrecl  20618  atanlogsublem  20622  efiatan2  20624  tanatan  20626  atandmtan  20627  cosatan  20628  cosatanne0  20629  wilthlem2  20719  ftalem7  20728  basellem2  20731  basellem4  20733  basellem5  20734  isppw  20764  dchrptlem2  20916  lgsne0  20984  2sqlem8a  21022  2sqlem8  21023  imadifxp  23881  xaddeq0  24030  xrge0iifhom  24127  logccne0OLD  24191  logbrec  24201  derangenlem  24636  subfacp1lem3  24647  subfacp1lem5  24649  prodfn0  25001  ntrivcvgtail  25007  fproddiv  25064  fprodn0  25082  nobndlem8  25377  itg2addnclem  25957  itg2addnclem2  25958  itg2addnc  25959  ivthALT  26029  neibastop1  26079  cmpfiiin  26442  pell1234qrne0  26607  rmxyneg  26674  bezoutr1  26742  fnwe2lem2  26817  kelac1  26830  frlmssuvc2  26916  pmtrmvd  27067  cnmsgnsubg  27103  stoweidlem31  27448  stoweidlem59  27476  wallispilem4  27485  wallispi  27487  stirlinglem3  27493  stirlinglem14  27504  vdn0frgrav2  27777  vdgn0frgrav2  27778  vdn1frgrav2  27779  vdgn1frgrav2  27780  lsatfixedN  29124  islshpat  29132  lkrshp  29220  2llnm3N  29683  dalemdnee  29780  cdleme18b  30406  cdleme40m  30581  cdlemg12g  30763  cdlemh  30931  cdlemj3  30937  tendoconid  30943  cdlemk3  30947  cdlemk12  30964  cdlemk12u  30986  cdlemk46  31062  cdlemk54  31072  erngdvlem4  31105  erngdvlem4-rN  31113  dibn0  31268  dihglblem2aN  31408  dochshpncl  31499  dochsnnz  31565  dochsatshpb  31567  lcfl7lem  31614  lcfl8b  31619  lcfrlem33  31690  lcfr  31700  hdmaprnlem3uN  31969
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 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380  df-ne 2552
  Copyright terms: Public domain W3C validator