Theorem eqnetrd 2675

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 2659	. 2 |- ( ph -> ( A =/= C <-> B =/= C ) )
4	1, 3	mpbird 232	1 |- ( ph -> A =/= C )

Syntax hints:   -> wi 4   = wceq 1399   =/= wne 2577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-cleq 2374  df-ne 2579

This theorem is referenced by:  eqnetrrd  2676  3netr4d  2687  opnz  4633  frsn  4984  xpdifid  5345  undefne0  6926  onoviun  6932  intrnfi  7791  cantnfp1lem2  8011  cantnfp1lem3  8012  cantnfp1lem2OLD  8037  cantnfp1lem3OLD  8038  wemapwe  8052  wemapweOLD  8053  acndom2  8348  fin23lem14  8626  fin23lem40  8644  isf32lem6  8651  isf34lem5  8671  isf34lem7  8672  isf34lem6  8673  axcc2lem  8729  xaddnemnf  11354  xaddnepnf  11355  fseqsupcl  11990  hashprg  12364  elprchashprn2  12365  limsupgre  13306  isercolllem3  13491  prodfn0  13705  ntrivcvgtail  13711  fproddiv  13768  fprodn0  13785  tanval3  13871  tanneg  13885  ruclem11  13975  phibndlem  14302  dfphi2  14306  0ram  14540  0ram2  14541  ram0  14542  0ramcl  14543  gsumval2  16024  sgrp2nmndlem5  16164  issubg2  16333  ghmrn  16397  pmtrmvd  16598  gsumval3OLD  17025  gsumval3  17028  pgpfaclem2  17246  ablfaclem2  17250  ablfaclem3  17251  abvdom  17600  lbsextlem2  17918  gzrngunit  18596  zringunit  18621  cnmsgnsubg  18704  frlmssuvc2  18915  iinopn  19496  cnconn  20008  1stcfb  20031  dissnlocfin  20115  fbasrn  20470  fclscmpi  20615  alexsublem  20629  ustuqtop5  20833  cnextucn  20891  dscmet  21178  reperflem  21408  evth  21544  cmetcaulem  21812  iscmet3  21817  cmetss  21838  bcthlem5  21852  bcth2  21854  mbflimsup  22158  itg1addlem4  22191  itg1climres  22206  itg2monolem1  22242  itg2i1fseq2  22248  tdeglem4  22543  deg1add  22589  deg1mul2  22600  deg1tm  22604  dgreq  22726  dgradd2  22750  dgrmul  22752  dgrmulc  22753  dgrcolem1  22755  plyrem  22786  facth  22787  fta1lem  22788  vieta1lem1  22791  vieta1lem2  22792  vieta1  22793  qaa  22804  aareccl  22807  geolim3  22820  aaliou3lem9  22831  coseq00topi  22980  cosne0  23002  tanord  23010  tanarg  23091  cxpne0  23145  cxpsqrt  23171  logbrec  23240  chordthmlem  23279  chordthmlem2  23280  dcubic  23293  mcubic  23294  cubic2  23295  cubic  23296  quartlem4  23307  atandmneg  23353  atandmcj  23356  atancj  23357  atanrecl  23358  atanlogsublem  23362  efiatan2  23364  tanatan  23366  atandmtan  23367  cosatan  23368  cosatanne0  23369  wilthlem2  23460  ftalem7  23469  basellem2  23472  basellem4  23474  basellem5  23475  isppw  23505  dchrptlem2  23657  lgsne0  23725  2sqlem8a  23763  2sqlem8  23764  tglnpt2  24141  midexlem  24189  colperpexlem3  24226  mideulem2  24228  lnopp2hpgb  24252  edgwlk  24652  wwlknext  24845  vdn0frgrav2  25144  vdgn0frgrav2  25145  vdn1frgrav2  25146  vdgn1frgrav2  25147  imadifxp  27591  acunirnmpt  27645  nn0sqeq1  27712  xaddeq0  27723  xrge0iifhom  28073  signswn0  28700  signsvtn0  28710  signstfvneq0  28712  derangenlem  28804  subfacp1lem3  28815  subfacp1lem5  28817  wsuclem  29546  nobndlem8  29624  tan2h  30212  heicant  30214  itg2addnclem2  30233  ivthALT  30319  neibastop1  30343  cmpfiiin  30795  pell1234qrne0  30954  rmxyneg  31021  bezoutr1  31089  fnwe2lem2  31163  kelac1  31175  radcnvrat  31363  binomcxplemfrat  31424  binomcxplemradcnv  31425  ioondisj2  31691  ioondisj1  31692  lptioo2  31803  lptioo1  31804  0ellimcdiv  31821  ioodvbdlimc1  31896  ioodvbdlimc2  31898  stoweidlem31  31979  stoweidlem59  32007  wallispilem4  32016  wallispi  32018  stirlinglem3  32024  stirlinglem14  32035  dirkerper  32044  dirkertrigeq  32049  dirkercncflem2  32052  fourierdlem4  32059  fourierdlem30  32085  fourierdlem41  32096  fourierdlem42  32097  fourierdlem44  32099  fourierdlem46  32101  fourierdlem48  32103  fourierdlem49  32104  fourierdlem62  32117  fourierdlem74  32129  fourierdlem75  32130  fourierdlem79  32134  fourierdlem102  32157  fourierdlem114  32169  fouriersw  32180  elaa2lem  32182  elaa2  32183  etransclem24  32207  etransclem44  32227  etransclem47  32230  lswn0  32554  pfxn0  32569  el0ldep  33267  islindeps2  33284  ldepsnlinclem1  33306  ldepsnlinclem2  33307  lsatfixedN  35147  islshpat  35155  lkrshp  35243  2llnm3N  35706  dalemdnee  35803  cdleme18b  36430  cdleme40m  36606  cdlemg12g  36788  cdlemh  36956  cdlemj3  36962  tendoconid  36968  cdlemk3  36972  cdlemk12  36989  cdlemk12u  37011  cdlemk46  37087  cdlemk54  37097  erngdvlem4  37130  erngdvlem4-rN  37138  dibn0  37293  dihglblem2aN  37433  dochshpncl  37524  dochsnnz  37590  dochsatshpb  37592  lcfl7lem  37639  lcfl8b  37644  lcfrlem33  37715  lcfr  37725  hdmaprnlem3uN  37994  wnefimgd  38503