Theorem eqnetrd 2999

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 2991	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqnetrrd  3000  3netr4d  3009  opnz  5448  xpdifid  6157  undefne0  8276  onoviun  8355  intrnfi  9426  cantnfp1lem2  9691  cantnfp1lem3  9692  wemapwe  9709  acndom2  10066  fin23lem14  10345  fin23lem40  10363  isf32lem6  10370  isf34lem5  10390  isf34lem7  10391  isf34lem6  10392  axcc2lem  10448  xaddnemnf  13250  xaddnepnf  13251  fseqsupcl  13993  hashprg  14411  elprchashprn2  14412  hash1n0  14437  limsupgre  15495  isercolllem3  15681  prodfn0  15908  ntrivcvgtail  15914  fproddiv  15975  fprodn0  15993  tanval3  16150  tanneg  16164  ruclem11  16256  nn0rppwr  16578  bezoutr1  16586  phibndlem  16787  dfphi2  16791  0ram  17038  0ram2  17039  ram0  17040  0ramcl  17041  gsumval2  18662  sgrp2nmndlem5  18905  issubg2  19122  ghmrn  19210  pmtrmvd  19435  gsumval3  19886  pgpfaclem2  20063  ablfaclem2  20067  ablfaclem3  20068  fincygsubgodd  20093  subdrgint  20761  abvdom  20788  lbsextlem2  21118  cndrng  21359  gzrngunit  21399  zringunit  21425  cnmsgnsubg  21535  frlmssuvc2  21753  mhpmulcl  22085  iinopn  22838  cnconn  23358  1stcfb  23381  dissnlocfin  23465  fbasrn  23820  fclscmpi  23965  alexsublem  23980  ustuqtop5  24182  cnextucn  24239  dscmet  24509  reperflem  24756  evth  24907  cmetcaulem  25238  iscmet3  25243  metsscmetcld  25265  cmetss  25266  bcthlem5  25278  bcth2  25280  mbflimsup  25617  itg1addlem4  25650  itg1climres  25665  itg2monolem1  25701  itg2i1fseq2  25707  tdeglem4  26015  deg1add  26058  deg1mul2  26069  deg1tm  26074  dgreq  26199  dgradd2  26224  dgrmul  26226  dgrmulc  26227  dgrcolem1  26229  plyrem  26263  facth  26264  fta1lem  26265  vieta1lem1  26268  vieta1lem2  26269  vieta1  26270  qaa  26281  aareccl  26284  geolim3  26297  aaliou3lem9  26308  coseq00topi  26461  cosne0  26488  tanord  26497  tanarg  26578  cxpne0  26636  cxpsqrt  26662  logbrec  26742  chordthmlem  26792  chordthmlem2  26793  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  quartlem4  26820  atandmneg  26866  atandmcj  26869  atancj  26870  atanrecl  26871  atanlogsublem  26875  efiatan2  26877  tanatan  26879  atandmtan  26880  cosatan  26881  cosatanne0  26882  wilthlem2  27029  ftalem7  27039  basellem2  27042  basellem4  27044  basellem5  27045  isppw  27074  dchrptlem2  27226  lgsne0  27296  2sqlem8a  27386  2sqlem8  27387  noseponlem  27626  tglnpt2  28566  midexlem  28617  colperpexlem3  28657  mideulem2  28659  lnopp2hpgb  28688  subgruhgredgd  29209  wwlksnext  29821  wspthsnonn0vne  29845  clwwisshclwws  29942  vdn0conngrumgrv2  30123  vdgn1frgrv2  30223  nrt2irr  30400  ifnetrue  32474  ifnefals  32475  imadifxp  32528  acunirnmpt  32583  fnpreimac  32595  quad3d  32673  xaddeq0  32676  pmtrcnelor  33048  domnprodn0  33216  qsidomlem2  33414  ply1dg3rt0irred  33541  m1pmeq  33542  ply1annnr  33683  minplyirred  33691  rtelextdg2lem  33706  constrrtcclem  33714  constrconj  33725  constrext2chnlem  33730  constrremulcl  33747  constrrecl  33749  constrreinvcl  33752  2sqr3minply  33760  2sqr3nconstr  33761  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminply  33768  cos9thpinconstrlem1  33769  madjusmdetlem2  33805  zar0ring  33855  xrge0iifhom  33914  signswn0  34538  signsvtn0  34548  signstfvneq0  34550  repr0  34589  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  wsuclem  35789  ivthALT  36299  neibastop1  36323  weiunfrlem  36428  finxpreclem2  37354  finxpreclem6  37360  tan2h  37582  poimirlem9  37599  heicant  37625  itg2addnclem2  37642  lsatfixedN  38973  islshpat  38981  lkrshp  39069  2llnm3N  39534  dalemdnee  39631  cdleme18b  40257  cdleme40m  40432  cdlemg12g  40614  cdlemh  40782  cdlemj3  40788  tendoconid  40794  cdlemk3  40798  cdlemk12  40815  cdlemk12u  40837  cdlemk46  40913  cdlemk54  40923  erngdvlem4  40956  erngdvlem4-rN  40964  dibn0  41118  dihglblem2aN  41258  dochshpncl  41349  dochsnnz  41415  dochsatshpb  41417  lcfl7lem  41464  lcfl8b  41469  lcfrlem33  41540  lcfr  41550  hdmaprnlem3uN  41816  aks4d1p1p7  42033  fldhmf1  42049  primrootspoweq0  42065  idomnnzpownz  42091  idomnnzgmulnz  42092  aks6d1c5lem2  42097  deg1gprod  42099  unitscyglem4  42157  metakunt7  42170  tanhalfpim  42345  remul01  42397  remulinvcom  42422  domnexpgn0cl  42493  ricdrng1  42498  prjcrv0  42603  3cubeslem2  42655  cmpfiiin  42667  pell1234qrne0  42823  rmxyneg  42891  fnwe2lem2  43022  kelac1  43034  wnefimgd  44132  radcnvrat  44286  binomcxplemfrat  44323  binomcxplemradcnv  44324  disjrnmpt2  45160  disjf1o  45163  choicefi  45172  ioondisj2  45470  ioondisj1  45471  lptioo2  45608  lptioo1  45609  0ellimcdiv  45626  liminflbuz2  45792  ioodvbdlimc1  45910  ioodvbdlimc2  45912  stoweidlem31  46008  stoweidlem59  46036  wallispilem4  46045  wallispi  46047  stirlinglem3  46053  stirlinglem14  46064  dirkerper  46073  dirkertrigeq  46078  dirkercncflem2  46081  fourierdlem4  46088  fourierdlem30  46114  fourierdlem41  46125  fourierdlem42  46126  fourierdlem44  46128  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem62  46145  fourierdlem74  46157  fourierdlem75  46158  fourierdlem79  46162  fourierdlem102  46185  fourierdlem114  46197  fouriersw  46208  elaa2lem  46210  elaa2  46211  etransclem24  46235  etransclem44  46255  etransclem47  46258  ioorrnopnlem  46281  subsaliuncl  46335  sge0cl  46358  meadjun  46439  meadjiunlem  46442  hoicvr  46525  ovnsubadd2lem  46622  smflimlem6  46753  smfpimcc  46785  smflimsuplem2  46798  lswn0  47406  sprvalpwn0  47445  fmtnoprmfac1lem  47526  grimuhgr  47848  gpg3nbgrvtx0  48026  el0ldep  48390  islindeps2  48407  ldepsnlinclem1  48429  ldepsnlinclem2  48430  itscnhlinecirc02plem1  48710  fvconstr  48786  fvconstrn0  48787  catprs  48934  fucofvalne  49184