Theorem eqnetrd 2718

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

Syntax hints:   -> wi 4   = wceq 1438   =/= wne 2619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-cleq 2415  df-ne 2621

This theorem is referenced by:  eqnetrrd  2719  3netr4d  2730  opnz  4691  frsn  4923  xpdifid  5283  undefne0  7036  onoviun  7072  intrnfi  7938  cantnfp1lem2  8191  cantnfp1lem3  8192  wemapwe  8209  acndom2  8491  fin23lem14  8769  fin23lem40  8787  isf32lem6  8794  isf34lem5  8814  isf34lem7  8815  isf34lem6  8816  axcc2lem  8872  xaddnemnf  11533  xaddnepnf  11534  fseqsupcl  12195  hashprg  12577  elprchashprn2  12578  limsupgre  13539  limsupgreOLD  13540  isercolllem3  13727  prodfn0  13947  ntrivcvgtail  13953  fproddiv  14012  fprodn0  14030  tanval3  14185  tanneg  14199  ruclem11  14289  phibndlem  14715  dfphi2  14719  0ram  14975  0ram2  14976  ram0  14977  0ramcl  14978  gsumval2  16520  sgrp2nmndlem5  16660  issubg2  16829  ghmrn  16893  pmtrmvd  17094  gsumval3  17538  pgpfaclem2  17712  ablfaclem2  17716  ablfaclem3  17717  abvdom  18063  lbsextlem2  18379  gzrngunit  19030  zringunit  19058  cnmsgnsubg  19141  frlmssuvc2  19349  iinopn  19928  cnconn  20433  1stcfb  20456  dissnlocfin  20540  fbasrn  20895  fclscmpi  21040  alexsublem  21055  ustuqtop5  21256  cnextucn  21314  dscmet  21583  reperflem  21832  evth  21983  cmetcaulem  22254  iscmet3  22259  cmetss  22280  bcthlem5  22292  bcth2  22294  mbflimsup  22619  mbflimsupOLD  22620  itg1addlem4  22653  itg1climres  22668  itg2monolem1  22704  itg2i1fseq2  22710  tdeglem4  23005  deg1add  23048  deg1mul2  23059  deg1tm  23063  dgreq  23194  dgradd2  23218  dgrmul  23220  dgrmulc  23221  dgrcolem1  23223  plyrem  23254  facth  23255  fta1lem  23256  vieta1lem1  23259  vieta1lem2  23260  vieta1  23261  qaa  23275  aareccl  23278  geolim3  23291  aaliou3lem9  23302  coseq00topi  23453  cosne0  23475  tanord  23483  tanarg  23564  cxpne0  23618  cxpsqrt  23644  logbrec  23715  chordthmlem  23754  chordthmlem2  23755  dcubic  23768  mcubic  23769  cubic2  23770  cubic  23771  quartlem4  23782  atandmneg  23828  atandmcj  23831  atancj  23832  atanrecl  23833  atanlogsublem  23837  efiatan2  23839  tanatan  23841  atandmtan  23842  cosatan  23843  cosatanne0  23844  wilthlem2  23990  ftalem7  24001  basellem2  24004  basellem4  24006  basellem5  24007  isppw  24037  dchrptlem2  24189  lgsne0  24257  2sqlem8a  24295  2sqlem8  24296  tglnpt2  24682  midexlem  24733  colperpexlem3  24770  mideulem2  24772  lnopp2hpgb  24801  edgwlk  25255  wwlknext  25448  vdn0frgrav2  25747  vdgn0frgrav2  25748  vdn1frgrav2  25749  vdgn1frgrav2  25750  imadifxp  28212  acunirnmpt  28261  nn0sqeq1  28328  xaddeq0  28334  madjusmdetlem2  28660  xrge0iifhom  28749  signswn0  29455  signsvtn0  29465  signstfvneq0  29467  derangenlem  29900  subfacp1lem3  29911  subfacp1lem5  29913  wsuclem  30513  nobndlem8  30591  ivthALT  30994  neibastop1  31018  finxpreclem2  31744  finxpreclem6  31750  tan2h  31899  poimirlem9  31911  heicant  31937  itg2addnclem2  31956  lsatfixedN  32542  islshpat  32550  lkrshp  32638  2llnm3N  33101  dalemdnee  33198  cdleme18b  33825  cdleme40m  34001  cdlemg12g  34183  cdlemh  34351  cdlemj3  34357  tendoconid  34363  cdlemk3  34367  cdlemk12  34384  cdlemk12u  34406  cdlemk46  34482  cdlemk54  34492  erngdvlem4  34525  erngdvlem4-rN  34533  dibn0  34688  dihglblem2aN  34828  dochshpncl  34919  dochsnnz  34985  dochsatshpb  34987  lcfl7lem  35034  lcfl8b  35039  lcfrlem33  35110  lcfr  35120  hdmaprnlem3uN  35389  cmpfiiin  35506  pell1234qrne0  35667  rmxyneg  35736  bezoutr1  35804  fnwe2lem2  35877  kelac1  35889  wnefimgd  36506  radcnvrat  36569  binomcxplemfrat  36606  binomcxplemradcnv  36607  disjrnmpt2  37361  disjf1o  37364  ioondisj2  37468  ioondisj1  37469  lptioo2  37579  lptioo1  37580  0ellimcdiv  37598  ioodvbdlimc1  37675  ioodvbdlimc2  37678  stoweidlem31  37760  stoweidlem59  37788  wallispilem4  37798  wallispi  37800  stirlinglem3  37806  stirlinglem14  37817  dirkerper  37826  dirkertrigeq  37831  dirkercncflem2  37834  fourierdlem4  37841  fourierdlem30  37867  fourierdlem41  37879  fourierdlem42  37880  fourierdlem42OLD  37881  fourierdlem44  37883  fourierdlem46  37884  fourierdlem48  37886  fourierdlem49  37887  fourierdlem62  37900  fourierdlem74  37912  fourierdlem75  37913  fourierdlem79  37917  fourierdlem102  37940  fourierdlem114  37952  fouriersw  37963  elaa2lem  37965  elaa2lemOLD  37966  elaa2  37967  etransclem24  37991  etransclem44  38011  etransclem47  38014  sge0cl  38059  meadjun  38127  meadjiunlem  38130  hoicvr  38193  lswn0  38680  pfxn0  38695  el0ldep  39653  islindeps2  39670  ldepsnlinclem1  39692  ldepsnlinclem2  39693