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  27892  midexlem  27943  colperpexlem3  27983  mideulem2  27985  lnopp2hpgb  28014  subgruhgredgd  28541  wwlksnext  29147  wspthsnonn0vne  29171  clwwisshclwws  29268  vdn0conngrumgrv2  29449  vdgn1frgrv2  29549  nrt2irr  29726  ifnetrue  31779  ifnefals  31780  imadifxp  31832  acunirnmpt  31884  fnpreimac  31896  xaddeq0  31966  pmtrcnelor  32252  qsidomlem2  32572  ply1annnr  32764  minplyirred  32770  madjusmdetlem2  32808  zar0ring  32858  xrge0iifhom  32917  signswn0  33571  signsvtn0  33581  signstfvneq0  33583  repr0  33623  derangenlem  34162  subfacp1lem3  34173  subfacp1lem5  34175  wsuclem  34797  ivthALT  35220  neibastop1  35244  finxpreclem2  36271  finxpreclem6  36277  tan2h  36480  poimirlem9  36497  heicant  36523  itg2addnclem2  36540  lsatfixedN  37879  islshpat  37887  lkrshp  37975  2llnm3N  38440  dalemdnee  38537  cdleme18b  39163  cdleme40m  39338  cdlemg12g  39520  cdlemh  39688  cdlemj3  39694  tendoconid  39700  cdlemk3  39704  cdlemk12  39721  cdlemk12u  39743  cdlemk46  39819  cdlemk54  39829  erngdvlem4  39862  erngdvlem4-rN  39870  dibn0  40024  dihglblem2aN  40164  dochshpncl  40255  dochsnnz  40321  dochsatshpb  40323  lcfl7lem  40370  lcfl8b  40375  lcfrlem33  40446  lcfr  40456  hdmaprnlem3uN  40722  aks4d1p1p7  40939  fldhmf1  40955  metakunt7  40991  ricdrng1  41102  nn0rppwr  41224  remul01  41280  remulinvcom  41305  prjcrv0  41375  3cubeslem2  41423  cmpfiiin  41435  pell1234qrne0  41591  rmxyneg  41659  fnwe2lem2  41793  kelac1  41805  wnefimgd  42913  radcnvrat  43073  binomcxplemfrat  43110  binomcxplemradcnv  43111  disjrnmpt2  43886  disjf1o  43889  choicefi  43899  ioondisj2  44206  ioondisj1  44207  lptioo2  44347  lptioo1  44348  0ellimcdiv  44365  liminflbuz2  44531  ioodvbdlimc1  44649  ioodvbdlimc2  44651  stoweidlem31  44747  stoweidlem59  44775  wallispilem4  44784  wallispi  44786  stirlinglem3  44792  stirlinglem14  44803  dirkerper  44812  dirkertrigeq  44817  dirkercncflem2  44820  fourierdlem4  44827  fourierdlem30  44853  fourierdlem41  44864  fourierdlem42  44865  fourierdlem44  44867  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem62  44884  fourierdlem74  44896  fourierdlem75  44897  fourierdlem79  44901  fourierdlem102  44924  fourierdlem114  44936  fouriersw  44947  elaa2lem  44949  elaa2  44950  etransclem24  44974  etransclem44  44994  etransclem47  44997  ioorrnopnlem  45020  subsaliuncl  45074  sge0cl  45097  meadjun  45178  meadjiunlem  45181  hoicvr  45264  ovnsubadd2lem  45361  smflimlem6  45492  smfpimcc  45524  smflimsuplem2  45537  lswn0  46112  sprvalpwn0  46151  fmtnoprmfac1lem  46232  el0ldep  47147  islindeps2  47164  ldepsnlinclem1  47186  ldepsnlinclem2  47187  itscnhlinecirc02plem1  47468  fvconstr  47522  fvconstrn0  47523  catprs  47631