Theorem eqnetrd 2849

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

Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  eqnetrrd  2850  3netr4d  2859  opnz  4868  xpdifid  5481  undefne0  7292  onoviun  7327  intrnfi  8205  cantnfp1lem2  8459  cantnfp1lem3  8460  wemapwe  8477  acndom2  8760  fin23lem14  9038  fin23lem40  9056  isf32lem6  9063  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  axcc2lem  9141  xaddnemnf  11941  xaddnepnf  11942  fseqsupcl  12638  hashprg  13043  hashprgOLD  13044  elprchashprn2  13045  limsupgre  14060  isercolllem3  14245  prodfn0  14465  ntrivcvgtail  14471  fproddiv  14530  fprodn0  14548  tanval3  14703  tanneg  14717  ruclem11  14808  bezoutr1  15120  phibndlem  15313  dfphi2  15317  0ram  15562  0ram2  15563  ram0  15564  0ramcl  15565  gsumval2  17103  sgrp2nmndlem5  17239  issubg2  17432  ghmrn  17496  pmtrmvd  17699  gsumval3  18131  pgpfaclem2  18304  ablfaclem2  18308  ablfaclem3  18309  abvdom  18661  lbsextlem2  18980  gzrngunit  19631  zringunit  19655  cnmsgnsubg  19742  frlmssuvc2  19953  iinopn  20532  cnconn  21035  1stcfb  21058  dissnlocfin  21142  fbasrn  21498  fclscmpi  21643  alexsublem  21658  ustuqtop5  21859  cnextucn  21917  dscmet  22187  reperflem  22429  evth  22566  cmetcaulem  22894  iscmet3  22899  cmetss  22921  bcthlem5  22933  bcth2  22935  mbflimsup  23239  itg1addlem4  23272  itg1climres  23287  itg2monolem1  23323  itg2i1fseq2  23329  tdeglem4  23624  deg1add  23667  deg1mul2  23678  deg1tm  23682  dgreq  23804  dgradd2  23828  dgrmul  23830  dgrmulc  23831  dgrcolem1  23833  plyrem  23864  facth  23865  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  vieta1  23871  qaa  23882  aareccl  23885  geolim3  23898  aaliou3lem9  23909  coseq00topi  24058  cosne0  24080  tanord  24088  tanarg  24169  cxpne0  24223  cxpsqrt  24249  logbrec  24320  chordthmlem  24359  chordthmlem2  24360  dcubic  24373  mcubic  24374  cubic2  24375  cubic  24376  quartlem4  24387  atandmneg  24433  atandmcj  24436  atancj  24437  atanrecl  24438  atanlogsublem  24442  efiatan2  24444  tanatan  24446  atandmtan  24447  cosatan  24448  cosatanne0  24449  wilthlem2  24595  ftalem7  24605  basellem2  24608  basellem4  24610  basellem5  24611  isppw  24640  dchrptlem2  24790  lgsne0  24860  2sqlem8a  24950  2sqlem8  24951  tglnpt2  25336  midexlem  25387  colperpexlem3  25424  mideulem2  25426  lnopp2hpgb  25455  edgwlk  26059  wwlknext  26252  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  imadifxp  28796  acunirnmpt  28841  nn0sqeq1  28901  xaddeq0  28907  madjusmdetlem2  29222  xrge0iifhom  29311  signswn0  29963  signsvtn0  29973  signstfvneq0  29975  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  wsuclem  31017  wsuclemOLD  31018  noseponlem  31065  nobndlem8  31098  ivthALT  31500  neibastop1  31524  finxpreclem2  32403  finxpreclem6  32409  tan2h  32571  poimirlem9  32588  heicant  32614  itg2addnclem2  32632  lsatfixedN  33314  islshpat  33322  lkrshp  33410  2llnm3N  33873  dalemdnee  33970  cdleme18b  34597  cdleme40m  34773  cdlemg12g  34955  cdlemh  35123  cdlemj3  35129  tendoconid  35135  cdlemk3  35139  cdlemk12  35156  cdlemk12u  35178  cdlemk46  35254  cdlemk54  35264  erngdvlem4  35297  erngdvlem4-rN  35305  dibn0  35460  dihglblem2aN  35600  dochshpncl  35691  dochsnnz  35757  dochsatshpb  35759  lcfl7lem  35806  lcfl8b  35811  lcfrlem33  35882  lcfr  35892  hdmaprnlem3uN  36161  cmpfiiin  36278  pell1234qrne0  36435  rmxyneg  36503  fnwe2lem2  36639  kelac1  36651  wnefimgd  37480  radcnvrat  37535  binomcxplemfrat  37572  binomcxplemradcnv  37573  disjrnmpt2  38370  disjf1o  38373  choicefi  38387  ioondisj2  38561  ioondisj1  38562  lptioo2  38698  lptioo1  38699  0ellimcdiv  38716  ioodvbdlimc1  38823  ioodvbdlimc2  38825  stoweidlem31  38924  stoweidlem59  38952  wallispilem4  38961  wallispi  38963  stirlinglem3  38969  stirlinglem14  38980  dirkerper  38989  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem4  39004  fourierdlem30  39030  fourierdlem41  39041  fourierdlem42  39042  fourierdlem44  39044  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem62  39061  fourierdlem74  39073  fourierdlem75  39074  fourierdlem79  39078  fourierdlem102  39101  fourierdlem114  39113  fouriersw  39124  elaa2lem  39126  elaa2  39127  etransclem24  39151  etransclem44  39171  etransclem47  39174  ioorrnopnlem  39200  subsaliuncl  39252  sge0cl  39274  meadjun  39355  meadjiunlem  39358  hoicvr  39438  ovnsubadd2lem  39535  smflimlem6  39662  fmtnoprmfac1lem  40014  lswn0  40242  pfxn0  40257  hash1n0  40370  subgruhgredgd  40508  wwlksnext  41099  wspthsnonn0vne  41124  clwwisshclwws  41235  vdn0conngrumgrv2  41363  vdgn1frgrv2  41466  el0ldep  42049  islindeps2  42066  ldepsnlinclem1  42088  ldepsnlinclem2  42089