Theorem eqnetrd 2760

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

Syntax hints:   -> wi 4   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  eqnetrrd  2761  3netr4d  2772  opnz  4724  frsn  5076  xpdifid  5441  xpimasnOLD  5459  undefne0  7020  onoviun  7026  intrnfi  7888  cantnfp1lem2  8110  cantnfp1lem3  8111  cantnfp1lem2OLD  8136  cantnfp1lem3OLD  8137  wemapwe  8151  wemapweOLD  8152  acndom2  8447  fin23lem14  8725  fin23lem40  8743  isf32lem6  8750  isf34lem5  8770  isf34lem7  8771  isf34lem6  8772  axcc2lem  8828  xaddnemnf  11445  xaddnepnf  11446  fseqsupcl  12067  hashprg  12440  elprchashprn2  12441  limsupgre  13283  isercolllem3  13468  tanval3  13746  tanneg  13760  ruclem11  13850  phibndlem  14175  dfphi2  14179  0ram  14413  0ram2  14414  ram0  14415  0ramcl  14416  gsumval2  15780  issubg2  16087  ghmrn  16151  pmtrmvd  16352  gsumval3OLD  16779  gsumval3  16782  pgpfaclem2  17003  ablfaclem2  17007  ablfaclem3  17008  abvdom  17356  lbsextlem2  17674  gzrngunit  18351  zringunit  18387  zrngunit  18388  cnmsgnsubg  18480  frlmssuvc2  18693  frlmssuvc2OLD  18695  iinopn  19278  cnconn  19789  1stcfb  19812  dissnlocfin  19896  fbasrn  20251  fclscmpi  20396  alexsublem  20410  ustuqtop5  20614  cnextucn  20672  dscmet  20959  reperflem  21189  evth  21325  cmetcaulem  21593  iscmet3  21598  cmetss  21619  bcthlem5  21633  bcth2  21635  mbflimsup  21939  itg1addlem4  21972  itg1climres  21987  itg2monolem1  22023  itg2i1fseq2  22029  tdeglem4  22324  deg1add  22370  deg1mul2  22381  deg1tm  22385  dgreq  22507  dgradd2  22530  dgrmul  22532  dgrmulc  22533  dgrcolem1  22535  plyrem  22566  facth  22567  fta1lem  22568  vieta1lem1  22571  vieta1lem2  22572  vieta1  22573  qaa  22584  aareccl  22587  geolim3  22600  aaliou3lem9  22611  coseq00topi  22759  cosne0  22781  tanord  22789  tanarg  22868  cxpne0  22922  cxpsqrt  22948  chordthmlem  23027  chordthmlem2  23028  dcubic  23041  mcubic  23042  cubic2  23043  cubic  23044  quartlem4  23055  atandmneg  23101  atandmcj  23104  atancj  23105  atanrecl  23106  atanlogsublem  23110  efiatan2  23112  tanatan  23114  atandmtan  23115  cosatan  23116  cosatanne0  23117  wilthlem2  23207  ftalem7  23216  basellem2  23219  basellem4  23221  basellem5  23222  isppw  23252  dchrptlem2  23404  lgsne0  23472  2sqlem8a  23510  2sqlem8  23511  tglnpt2  23879  midexlem  23924  colperpexlem3  23958  mideulem2  23960  edgwlk  24363  wwlknext  24556  vdn0frgrav2  24855  vdgn0frgrav2  24856  vdn1frgrav2  24857  vdgn1frgrav2  24858  imadifxp  27289  nn0sqeq1  27393  xaddeq0  27404  xrge0iifhom  27751  logccne0OLD  27843  logbrec  27853  signswn0  28349  signsvtn0  28359  signstfvneq0  28361  derangenlem  28447  subfacp1lem3  28458  subfacp1lem5  28460  prodfn0  28962  ntrivcvgtail  28968  fproddiv  29025  fprodn0  29043  wsuclem  29315  nobndlem8  29393  tan2h  29981  heicant  29983  itg2addnclem2  30001  ivthALT  30087  neibastop1  30111  cmpfiiin  30563  pell1234qrne0  30723  rmxyneg  30790  bezoutr1  30858  fnwe2lem2  30931  kelac1  30943  ioondisj2  31418  ioondisj1  31419  lptioo2  31502  lptioo1  31503  0ellimcdiv  31520  ioodvbdlimc1  31592  ioodvbdlimc2  31594  stoweidlem31  31660  stoweidlem59  31688  wallispilem4  31697  wallispi  31699  stirlinglem3  31705  stirlinglem14  31716  dirkerper  31725  dirkertrigeq  31730  dirkercncflem2  31733  fourierdlem4  31740  fourierdlem30  31766  fourierdlem41  31777  fourierdlem42  31778  fourierdlem44  31780  fourierdlem46  31782  fourierdlem48  31784  fourierdlem49  31785  fourierdlem62  31798  fourierdlem74  31810  fourierdlem75  31811  fourierdlem79  31815  fourierdlem102  31838  fourierdlem114  31850  fouriersw  31861  lswn0  32139  sgrp2nmndlem5ALT  32262  el0ldep  32554  islindeps2  32571  ldepsnlinclem1  32593  ldepsnlinclem2  32594  lsatfixedN  34212  islshpat  34220  lkrshp  34308  2llnm3N  34771  dalemdnee  34868  cdleme18b  35494  cdleme40m  35669  cdlemg12g  35851  cdlemh  36019  cdlemj3  36025  tendoconid  36031  cdlemk3  36035  cdlemk12  36052  cdlemk12u  36074  cdlemk46  36150  cdlemk54  36160  erngdvlem4  36193  erngdvlem4-rN  36201  dibn0  36356  dihglblem2aN  36496  dochshpncl  36587  dochsnnz  36653  dochsatshpb  36655  lcfl7lem  36702  lcfl8b  36707  lcfrlem33  36778  lcfr  36788  hdmaprnlem3uN  37057