Theorem eqnetrd 3009

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  eqnetrrd  3010  3netr4d  3019  opnz  5474  xpdifid  6168  undefne0  8264  onoviun  8343  intrnfi  9411  cantnfp1lem2  9674  cantnfp1lem3  9675  wemapwe  9692  acndom2  10049  fin23lem14  10328  fin23lem40  10346  isf32lem6  10353  isf34lem5  10373  isf34lem7  10374  isf34lem6  10375  axcc2lem  10431  xaddnemnf  13215  xaddnepnf  13216  fseqsupcl  13942  hashprg  14355  elprchashprn2  14356  hash1n0  14381  limsupgre  15425  isercolllem3  15613  prodfn0  15840  ntrivcvgtail  15846  fproddiv  15905  fprodn0  15923  tanval3  16077  tanneg  16091  ruclem11  16183  bezoutr1  16506  phibndlem  16703  dfphi2  16707  0ram  16953  0ram2  16954  ram0  16955  0ramcl  16956  gsumval2  18605  sgrp2nmndlem5  18810  issubg2  19021  ghmrn  19105  pmtrmvd  19324  gsumval3  19775  pgpfaclem2  19952  ablfaclem2  19956  ablfaclem3  19957  fincygsubgodd  19982  subdrgint  20419  abvdom  20446  lbsextlem2  20772  gzrngunit  21011  zringunit  21036  cnmsgnsubg  21130  frlmssuvc2  21350  mhpmulcl  21692  iinopn  22404  cnconn  22926  1stcfb  22949  dissnlocfin  23033  fbasrn  23388  fclscmpi  23533  alexsublem  23548  ustuqtop5  23750  cnextucn  23808  dscmet  24081  reperflem  24334  evth  24475  cmetcaulem  24805  iscmet3  24810  metsscmetcld  24832  cmetss  24833  bcthlem5  24845  bcth2  24847  mbflimsup  25183  itg1addlem4  25216  itg1addlem4OLD  25217  itg1climres  25232  itg2monolem1  25268  itg2i1fseq2  25274  tdeglem4  25577  tdeglem4OLD  25578  deg1add  25621  deg1mul2  25632  deg1tm  25636  dgreq  25758  dgradd2  25782  dgrmul  25784  dgrmulc  25785  dgrcolem1  25787  plyrem  25818  facth  25819  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  vieta1  25825  qaa  25836  aareccl  25839  geolim3  25852  aaliou3lem9  25863  coseq00topi  26012  cosne0  26038  tanord  26047  tanarg  26127  cxpne0  26185  cxpsqrt  26211  logbrec  26287  chordthmlem  26337  chordthmlem2  26338  dcubic  26351  mcubic  26352  cubic2  26353  cubic  26354  quartlem4  26365  atandmneg  26411  atandmcj  26414  atancj  26415  atanrecl  26416  atanlogsublem  26420  efiatan2  26422  tanatan  26424  atandmtan  26425  cosatan  26426  cosatanne0  26427  wilthlem2  26573  ftalem7  26583  basellem2  26586  basellem4  26588  basellem5  26589  isppw  26618  dchrptlem2  26768  lgsne0  26838  2sqlem8a  26928  2sqlem8  26929  noseponlem  27167  tglnpt2  27923  midexlem  27974  colperpexlem3  28014  mideulem2  28016  lnopp2hpgb  28045  subgruhgredgd  28572  wwlksnext  29178  wspthsnonn0vne  29202  clwwisshclwws  29299  vdn0conngrumgrv2  29480  vdgn1frgrv2  29580  nrt2irr  29757  ifnetrue  31810  ifnefals  31811  imadifxp  31863  acunirnmpt  31915  fnpreimac  31927  xaddeq0  31997  pmtrcnelor  32283  qsidomlem2  32603  ply1annnr  32795  minplyirred  32801  madjusmdetlem2  32839  zar0ring  32889  xrge0iifhom  32948  signswn0  33602  signsvtn0  33612  signstfvneq0  33614  repr0  33654  derangenlem  34193  subfacp1lem3  34204  subfacp1lem5  34206  wsuclem  34828  ivthALT  35268  neibastop1  35292  finxpreclem2  36319  finxpreclem6  36325  tan2h  36528  poimirlem9  36545  heicant  36571  itg2addnclem2  36588  lsatfixedN  37927  islshpat  37935  lkrshp  38023  2llnm3N  38488  dalemdnee  38585  cdleme18b  39211  cdleme40m  39386  cdlemg12g  39568  cdlemh  39736  cdlemj3  39742  tendoconid  39748  cdlemk3  39752  cdlemk12  39769  cdlemk12u  39791  cdlemk46  39867  cdlemk54  39877  erngdvlem4  39910  erngdvlem4-rN  39918  dibn0  40072  dihglblem2aN  40212  dochshpncl  40303  dochsnnz  40369  dochsatshpb  40371  lcfl7lem  40418  lcfl8b  40423  lcfrlem33  40494  lcfr  40504  hdmaprnlem3uN  40770  aks4d1p1p7  40987  fldhmf1  41003  metakunt7  41039  ricdrng1  41150  nn0rppwr  41272  remul01  41328  remulinvcom  41353  prjcrv0  41423  3cubeslem2  41471  cmpfiiin  41483  pell1234qrne0  41639  rmxyneg  41707  fnwe2lem2  41841  kelac1  41853  wnefimgd  42961  radcnvrat  43121  binomcxplemfrat  43158  binomcxplemradcnv  43159  disjrnmpt2  43934  disjf1o  43937  choicefi  43947  ioondisj2  44254  ioondisj1  44255  lptioo2  44395  lptioo1  44396  0ellimcdiv  44413  liminflbuz2  44579  ioodvbdlimc1  44697  ioodvbdlimc2  44699  stoweidlem31  44795  stoweidlem59  44823  wallispilem4  44832  wallispi  44834  stirlinglem3  44840  stirlinglem14  44851  dirkerper  44860  dirkertrigeq  44865  dirkercncflem2  44868  fourierdlem4  44875  fourierdlem30  44901  fourierdlem41  44912  fourierdlem42  44913  fourierdlem44  44915  fourierdlem46  44916  fourierdlem48  44918  fourierdlem49  44919  fourierdlem62  44932  fourierdlem74  44944  fourierdlem75  44945  fourierdlem79  44949  fourierdlem102  44972  fourierdlem114  44984  fouriersw  44995  elaa2lem  44997  elaa2  44998  etransclem24  45022  etransclem44  45042  etransclem47  45045  ioorrnopnlem  45068  subsaliuncl  45122  sge0cl  45145  meadjun  45226  meadjiunlem  45229  hoicvr  45312  ovnsubadd2lem  45409  smflimlem6  45540  smfpimcc  45572  smflimsuplem2  45585  lswn0  46160  sprvalpwn0  46199  fmtnoprmfac1lem  46280  el0ldep  47195  islindeps2  47212  ldepsnlinclem1  47234  ldepsnlinclem2  47235  itscnhlinecirc02plem1  47516  fvconstr  47570  fvconstrn0  47571  catprs  47679