Theorem eqnetrd 2585

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

Step	Hyp	Ref	Expression
1		eqnetrd.2	. 2 |- ( ph -> B =/= C )
2		eqnetrd.1	. . 3 |- ( ph -> A = B )
3	2	neeq1d 2580	. 2 |- ( ph -> ( A =/= C <-> B =/= C ) )
4	1, 3	mpbird 224	1 |- ( ph -> A =/= C )

Syntax hints:   -> wi 4   = wceq 1649   =/= wne 2567

This theorem is referenced by:  eqnetrrd  2587  opnz  4392  frsn  4907  xpimasn  5275  onoviun  6564  intrnfi  7379  cantnfp1lem2  7591  cantnfp1lem3  7592  wemapwe  7610  acndom2  7891  fin23lem14  8169  fin23lem40  8187  isf32lem6  8194  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  axcc2lem  8272  xaddnemnf  10776  xaddnepnf  10777  fseqsupcl  11271  hashprg  11621  elprchashprn2  11622  limsupgre  12230  isercolllem3  12415  tanval3  12690  tanneg  12704  ruclem11  12794  phibndlem  13114  dfphi2  13118  0ram  13343  0ram2  13344  ram0  13345  0ramcl  13346  gsumval2  14738  issubg2  14914  ghmrn  14974  gsumval3  15469  pgpfaclem2  15595  ablfaclem2  15599  ablfaclem3  15600  abvdom  15881  lbsextlem2  16186  gzrngunit  16719  zrngunit  16720  iinopn  16930  cnconn  17438  1stcfb  17461  fbasrn  17869  fclscmpi  18014  alexsublem  18028  ustuqtop5  18228  cnextucn  18286  dscmet  18573  reperflem  18802  evth  18937  cmetcaulem  19194  iscmet3  19199  cmetss  19220  bcthlem5  19234  bcth2  19236  mbflimsup  19511  itg1addlem4  19544  itg1climres  19559  itg2monolem1  19595  itg2i1fseq2  19601  tdeglem4  19936  deg1add  19979  deg1mul2  19990  deg1tm  19994  dgreq  20116  dgradd2  20139  dgrmul  20141  dgrmulc  20142  dgrcolem1  20144  plyrem  20175  facth  20176  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  qaa  20193  aareccl  20196  geolim3  20209  aaliou3lem9  20220  coseq00topi  20363  cosne0  20385  tanord  20393  tanarg  20467  cxpne0  20521  cxpsqr  20547  chordthmlem  20626  chordthmlem2  20627  dcubic  20639  mcubic  20640  cubic2  20641  cubic  20642  quartlem4  20653  atandmneg  20699  atandmcj  20702  atancj  20703  atanrecl  20704  atanlogsublem  20708  efiatan2  20710  tanatan  20712  atandmtan  20713  cosatan  20714  cosatanne0  20715  wilthlem2  20805  ftalem7  20814  basellem2  20817  basellem4  20819  basellem5  20820  isppw  20850  dchrptlem2  21002  lgsne0  21070  2sqlem8a  21108  2sqlem8  21109  imadifxp  23991  xaddeq0  24072  xrge0iifhom  24276  logccne0OLD  24348  logbrec  24358  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  prodfn0  25175  ntrivcvgtail  25181  fproddiv  25238  fprodn0  25256  nobndlem8  25567  itg2addnclem2  26156  ivthALT  26228  neibastop1  26278  cmpfiiin  26641  pell1234qrne0  26806  rmxyneg  26873  bezoutr1  26941  fnwe2lem2  27016  kelac1  27029  frlmssuvc2  27115  pmtrmvd  27266  cnmsgnsubg  27302  stoweidlem31  27647  stoweidlem59  27675  wallispilem4  27684  wallispi  27686  stirlinglem3  27692  stirlinglem14  27703  vdn0frgrav2  28128  vdgn0frgrav2  28129  vdn1frgrav2  28130  vdgn1frgrav2  28131  lsatfixedN  29492  islshpat  29500  lkrshp  29588  2llnm3N  30051  dalemdnee  30148  cdleme18b  30774  cdleme40m  30949  cdlemg12g  31131  cdlemh  31299  cdlemj3  31305  tendoconid  31311  cdlemk3  31315  cdlemk12  31332  cdlemk12u  31354  cdlemk46  31430  cdlemk54  31440  erngdvlem4  31473  erngdvlem4-rN  31481  dibn0  31636  dihglblem2aN  31776  dochshpncl  31867  dochsnnz  31933  dochsatshpb  31935  lcfl7lem  31982  lcfl8b  31987  lcfrlem33  32058  lcfr  32068  hdmaprnlem3uN  32337

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 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397  df-ne 2569