Theorem eqnetrd 2993

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqnetrd.2	⊢ (𝜑 → 𝐵 ≠ 𝐶)

Assertion

Ref	Expression
eqnetrd	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem eqnetrd

Step	Hyp	Ref	Expression
1		eqnetrd.2	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
2		eqnetrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	neeq1d 2985	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  eqnetrrd  2994  3netr4d  3003  opnz  5436  xpdifid  6144  undefne0  8261  onoviun  8315  intrnfi  9374  cantnfp1lem2  9639  cantnfp1lem3  9640  wemapwe  9657  acndom2  10014  fin23lem14  10293  fin23lem40  10311  isf32lem6  10318  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  axcc2lem  10396  xaddnemnf  13203  xaddnepnf  13204  fseqsupcl  13949  hashprg  14367  elprchashprn2  14368  hash1n0  14393  limsupgre  15454  isercolllem3  15640  prodfn0  15867  ntrivcvgtail  15873  fproddiv  15934  fprodn0  15952  tanval3  16109  tanneg  16123  ruclem11  16215  nn0rppwr  16538  bezoutr1  16546  phibndlem  16747  dfphi2  16751  0ram  16998  0ram2  16999  ram0  17000  0ramcl  17001  gsumval2  18620  sgrp2nmndlem5  18863  issubg2  19080  ghmrn  19168  pmtrmvd  19393  gsumval3  19844  pgpfaclem2  20021  ablfaclem2  20025  ablfaclem3  20026  fincygsubgodd  20051  subdrgint  20719  abvdom  20746  lbsextlem2  21076  cndrng  21317  gzrngunit  21357  zringunit  21383  cnmsgnsubg  21493  frlmssuvc2  21711  mhpmulcl  22043  iinopn  22796  cnconn  23316  1stcfb  23339  dissnlocfin  23423  fbasrn  23778  fclscmpi  23923  alexsublem  23938  ustuqtop5  24140  cnextucn  24197  dscmet  24467  reperflem  24714  evth  24865  cmetcaulem  25195  iscmet3  25200  metsscmetcld  25222  cmetss  25223  bcthlem5  25235  bcth2  25237  mbflimsup  25574  itg1addlem4  25607  itg1climres  25622  itg2monolem1  25658  itg2i1fseq2  25664  tdeglem4  25972  deg1add  26015  deg1mul2  26026  deg1tm  26031  dgreq  26156  dgradd2  26181  dgrmul  26183  dgrmulc  26184  dgrcolem1  26186  plyrem  26220  facth  26221  fta1lem  26222  vieta1lem1  26225  vieta1lem2  26226  vieta1  26227  qaa  26238  aareccl  26241  geolim3  26254  aaliou3lem9  26265  coseq00topi  26418  cosne0  26445  tanord  26454  tanarg  26535  cxpne0  26593  cxpsqrt  26619  logbrec  26699  chordthmlem  26749  chordthmlem2  26750  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  quartlem4  26777  atandmneg  26823  atandmcj  26826  atancj  26827  atanrecl  26828  atanlogsublem  26832  efiatan2  26834  tanatan  26836  atandmtan  26837  cosatan  26838  cosatanne0  26839  wilthlem2  26986  ftalem7  26996  basellem2  26999  basellem4  27001  basellem5  27002  isppw  27031  dchrptlem2  27183  lgsne0  27253  2sqlem8a  27343  2sqlem8  27344  noseponlem  27583  recsne0  28102  tglnpt2  28575  midexlem  28626  colperpexlem3  28666  mideulem2  28668  lnopp2hpgb  28697  subgruhgredgd  29218  wwlksnext  29830  wspthsnonn0vne  29854  clwwisshclwws  29951  vdn0conngrumgrv2  30132  vdgn1frgrv2  30232  nrt2irr  30409  ifnetrue  32483  ifnefals  32484  imadifxp  32537  acunirnmpt  32590  fnpreimac  32602  quad3d  32680  xaddeq0  32683  pmtrcnelor  33055  domnprodn0  33233  qsidomlem2  33431  ply1dg3rt0irred  33558  m1pmeq  33559  ply1annnr  33700  minplyirred  33708  rtelextdg2lem  33723  constrrtcclem  33731  constrconj  33742  constrext2chnlem  33747  constrremulcl  33764  constrrecl  33766  constrreinvcl  33769  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminply  33785  cos9thpinconstrlem1  33786  cos9thpinconstrlem2  33787  cos9thpinconstr  33788  madjusmdetlem2  33825  zar0ring  33875  xrge0iifhom  33934  signswn0  34558  signsvtn0  34568  signstfvneq0  34570  repr0  34609  derangenlem  35165  subfacp1lem3  35176  subfacp1lem5  35178  wsuclem  35820  ivthALT  36330  neibastop1  36354  weiunfrlem  36459  finxpreclem2  37385  finxpreclem6  37391  tan2h  37613  poimirlem9  37630  heicant  37656  itg2addnclem2  37673  lsatfixedN  39009  islshpat  39017  lkrshp  39105  2llnm3N  39570  dalemdnee  39667  cdleme18b  40293  cdleme40m  40468  cdlemg12g  40650  cdlemh  40818  cdlemj3  40824  tendoconid  40830  cdlemk3  40834  cdlemk12  40851  cdlemk12u  40873  cdlemk46  40949  cdlemk54  40959  erngdvlem4  40992  erngdvlem4-rN  41000  dibn0  41154  dihglblem2aN  41294  dochshpncl  41385  dochsnnz  41451  dochsatshpb  41453  lcfl7lem  41500  lcfl8b  41505  lcfrlem33  41576  lcfr  41586  hdmaprnlem3uN  41852  aks4d1p1p7  42069  fldhmf1  42085  primrootspoweq0  42101  idomnnzpownz  42127  idomnnzgmulnz  42128  aks6d1c5lem2  42133  deg1gprod  42135  unitscyglem4  42193  tanhalfpim  42344  remul01  42402  remulinvcom  42428  domnexpgn0cl  42518  ricdrng1  42523  prjcrv0  42628  3cubeslem2  42680  cmpfiiin  42692  pell1234qrne0  42848  rmxyneg  42916  fnwe2lem2  43047  kelac1  43059  wnefimgd  44157  radcnvrat  44310  binomcxplemfrat  44347  binomcxplemradcnv  44348  disjrnmpt2  45189  disjf1o  45192  choicefi  45201  ioondisj2  45498  ioondisj1  45499  lptioo2  45636  lptioo1  45637  0ellimcdiv  45654  liminflbuz2  45820  ioodvbdlimc1  45938  ioodvbdlimc2  45940  stoweidlem31  46036  stoweidlem59  46064  wallispilem4  46073  wallispi  46075  stirlinglem3  46081  stirlinglem14  46092  dirkerper  46101  dirkertrigeq  46106  dirkercncflem2  46109  fourierdlem4  46116  fourierdlem30  46142  fourierdlem41  46153  fourierdlem42  46154  fourierdlem44  46156  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem62  46173  fourierdlem74  46185  fourierdlem75  46186  fourierdlem79  46190  fourierdlem102  46213  fourierdlem114  46225  fouriersw  46236  elaa2lem  46238  elaa2  46239  etransclem24  46263  etransclem44  46283  etransclem47  46286  ioorrnopnlem  46309  subsaliuncl  46363  sge0cl  46386  meadjun  46467  meadjiunlem  46470  hoicvr  46553  ovnsubadd2lem  46650  smflimlem6  46781  smfpimcc  46813  smflimsuplem2  46826  modm2nep1  47371  modm1nep2  47373  modm1p1ne  47375  lswn0  47449  sprvalpwn0  47488  fmtnoprmfac1lem  47569  grimuhgr  47891  gpg3nbgrvtx0  48071  el0ldep  48459  islindeps2  48476  ldepsnlinclem1  48498  ldepsnlinclem2  48499  itscnhlinecirc02plem1  48775  fvconstr  48854  fvconstrn0  48855  catprs  49004  fucofvalne  49318