Theorem eqnetrrd 3001

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

Hypotheses

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

Assertion

Ref	Expression
eqnetrrd	⊢ (𝜑 → 𝐵 ≠ 𝐶)

Proof of Theorem eqnetrrd

Step	Hyp	Ref	Expression
1		eqnetrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2743	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqnetrrd.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
4	2, 3	eqnetrd 3000	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  eqnetrrid  3008  3netr3d  3009  cantnflem1c  9608  eqsqrt2d  15304  tanval2  16070  tanval3  16071  tanhlt1  16097  pcadd  16829  efgsres  19679  gsumval3  19848  ablfac  20031  ablsimpgfind  20053  isdrngrd  20711  isdrngrdOLD  20713  lspsneq  21089  lebnumlem3  24930  minveclem4a  25398  evthicc  25428  ioorf  25542  deg1ldgn  26066  fta1blem  26144  vieta1lem1  26286  vieta1lem2  26287  vieta1  26288  tanregt0  26516  isosctrlem2  26797  angpieqvd  26809  chordthmlem2  26811  dcubic2  26822  dquartlem1  26829  dquart  26831  asinlem  26846  atandmcj  26887  2efiatan  26896  tanatan  26897  dvatan  26913  dmgmn0  27004  dmgmdivn0  27006  lgamgulmlem2  27008  gamne0  27024  nosep1o  27661  noetasuplem4  27716  footexALT  28802  footexlem1  28803  footexlem2  28804  ttgcontlem1  28969  wlkn0  29706  nrt2irr  30560  fsuppcurry1  32814  fsuppcurry2  32815  bcm1n  32886  mxidlirred  33565  dfufd2  33643  ply1dg1rt  33673  esplymhp  33745  irngnminplynz  33890  minplym1p  33891  minplynzm1p  33892  algextdeglem4  33898  constrrtll  33909  constrrtlc1  33910  constrrtcclem  33912  constrfin  33924  constrelextdg2  33925  cos9thpiminplylem2  33961  zarclssn  34051  sibfof  34518  finxpreclem2  37645  poimirlem9  37880  heicant  37906  heiborlem6  38067  lkrlspeqN  39547  cdlemg18d  41057  cdlemg21  41062  dibord  41535  lclkrlem2u  41903  lcfrlem9  41926  mapdindp4  42099  hdmaprnlem3uN  42227  hdmaprnlem9N  42233  fsuppind  42948  binomcxplemnotnn0  44712  dstregt0  45644  stoweidlem31  46389  stoweidlem59  46417  wallispilem4  46426  dirkertrigeqlem2  46457  fourierdlem43  46508  fourierdlem65  46529  catprs  49370  oppfrcl3  49489  lmdran  50030  cmdlan  50031