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

Theorem eqnetrd 2561
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 2556 . 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 2543
This theorem is referenced by:  eqnetrrd  2563  opnz  4366  frsn  4881  xpimasn  5249  onoviun  6534  intrnfi  7349  cantnfp1lem2  7561  cantnfp1lem3  7562  wemapwe  7580  acndom2  7861  fin23lem14  8139  fin23lem40  8157  isf32lem6  8164  isf34lem5  8184  isf34lem7  8185  isf34lem6  8186  axcc2lem  8242  xaddnemnf  10745  xaddnepnf  10746  fseqsupcl  11236  hashprg  11586  elprchashprn2  11587  limsupgre  12195  isercolllem3  12380  tanval3  12655  tanneg  12669  ruclem11  12759  phibndlem  13079  dfphi2  13083  0ram  13308  0ram2  13309  ram0  13310  0ramcl  13311  gsumval2  14703  issubg2  14879  ghmrn  14939  gsumval3  15434  pgpfaclem2  15560  ablfaclem2  15564  ablfaclem3  15565  abvdom  15846  lbsextlem2  16151  gzrngunit  16680  zrngunit  16681  iinopn  16891  cnconn  17399  1stcfb  17422  fbasrn  17830  fclscmpi  17975  alexsublem  17989  ustuqtop5  18189  cnextucn  18247  dscmet  18484  reperflem  18713  evth  18848  cmetcaulem  19105  iscmet3  19110  cmetss  19131  bcthlem5  19143  bcth2  19145  mbflimsup  19418  itg1addlem4  19451  itg1climres  19466  itg2monolem1  19502  itg2i1fseq2  19508  tdeglem4  19843  deg1add  19886  deg1mul2  19897  deg1tm  19901  dgreq  20023  dgradd2  20046  dgrmul  20048  dgrmulc  20049  dgrcolem1  20051  plyrem  20082  facth  20083  fta1lem  20084  vieta1lem1  20087  vieta1lem2  20088  vieta1  20089  qaa  20100  aareccl  20103  geolim3  20116  aaliou3lem9  20127  coseq00topi  20270  cosne0  20292  tanord  20300  tanarg  20374  cxpne0  20428  cxpsqr  20454  chordthmlem  20533  chordthmlem2  20534  dcubic  20546  mcubic  20547  cubic2  20548  cubic  20549  quartlem4  20560  atandmneg  20606  atandmcj  20609  atancj  20610  atanrecl  20611  atanlogsublem  20615  efiatan2  20617  tanatan  20619  atandmtan  20620  cosatan  20621  cosatanne0  20622  wilthlem2  20712  ftalem7  20721  basellem2  20724  basellem4  20726  basellem5  20727  isppw  20757  dchrptlem2  20909  lgsne0  20977  2sqlem8a  21015  2sqlem8  21016  imadifxp  23874  xaddeq0  24023  xrge0iifhom  24120  logccne0OLD  24184  logbrec  24194  derangenlem  24629  subfacp1lem3  24640  subfacp1lem5  24642  prodfn0  24994  ntrivcvgtail  25000  fproddiv  25057  fprodn0  25075  nobndlem8  25370  itg2addnclem  25950  itg2addnclem2  25951  itg2addnc  25952  ivthALT  26022  neibastop1  26072  cmpfiiin  26435  pell1234qrne0  26600  rmxyneg  26667  bezoutr1  26735  fnwe2lem2  26810  kelac1  26823  frlmssuvc2  26909  pmtrmvd  27060  cnmsgnsubg  27096  stoweidlem31  27441  stoweidlem59  27469  wallispilem4  27478  wallispi  27480  stirlinglem3  27486  stirlinglem14  27497  vdn0frgrav2  27770  vdgn0frgrav2  27771  vdn1frgrav2  27772  vdgn1frgrav2  27773  lsatfixedN  29175  islshpat  29183  lkrshp  29271  2llnm3N  29734  dalemdnee  29831  cdleme18b  30457  cdleme40m  30632  cdlemg12g  30814  cdlemh  30982  cdlemj3  30988  tendoconid  30994  cdlemk3  30998  cdlemk12  31015  cdlemk12u  31037  cdlemk46  31113  cdlemk54  31123  erngdvlem4  31156  erngdvlem4-rN  31164  dibn0  31319  dihglblem2aN  31459  dochshpncl  31550  dochsnnz  31616  dochsatshpb  31618  lcfl7lem  31665  lcfl8b  31670  lcfrlem33  31741  lcfr  31751  hdmaprnlem3uN  32020
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 2361
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2373  df-ne 2545
  Copyright terms: Public domain W3C validator