Theorem eqnetrrd 3002

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 2745	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqnetrrd.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
4	2, 3	eqnetrd 3001	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  eqnetrrid  3009  3netr3d  3010  cantnflem1c  9599  eqsqrt2d  15322  tanval2  16091  tanval3  16092  tanhlt1  16118  pcadd  16851  efgsres  19704  gsumval3  19873  ablfac  20056  ablsimpgfind  20078  isdrngrd  20738  isdrngrdOLD  20740  lspsneq  21115  lebnumlem3  24948  minveclem4a  25415  evthicc  25444  ioorf  25558  deg1ldgn  26076  fta1blem  26154  vieta1lem1  26294  vieta1lem2  26295  vieta1  26296  tanregt0  26521  isosctrlem2  26801  angpieqvd  26813  chordthmlem2  26815  dcubic2  26826  dquartlem1  26833  dquart  26835  asinlem  26850  atandmcj  26891  2efiatan  26900  tanatan  26901  dvatan  26917  dmgmn0  27007  dmgmdivn0  27009  lgamgulmlem2  27011  gamne0  27027  nosep1o  27663  noetasuplem4  27718  footexALT  28804  footexlem1  28805  footexlem2  28806  ttgcontlem1  28971  wlkn0  29707  nrt2irr  30561  fsuppcurry1  32816  fsuppcurry2  32817  bcm1n  32887  mxidlirred  33555  dfufd2  33633  ply1dg1rt  33663  esplymhp  33752  irngnminplynz  33896  minplym1p  33897  minplynzm1p  33898  algextdeglem4  33904  constrrtll  33915  constrrtlc1  33916  constrrtcclem  33918  constrfin  33930  constrelextdg2  33931  cos9thpiminplylem2  33967  zarclssn  34057  sibfof  34524  finxpreclem2  37752  poimirlem9  37996  heicant  38022  heiborlem6  38183  lkrlspeqN  39663  cdlemg18d  41173  cdlemg21  41178  dibord  41651  lclkrlem2u  42019  lcfrlem9  42042  mapdindp4  42215  hdmaprnlem3uN  42343  hdmaprnlem9N  42349  fsuppind  43040  binomcxplemnotnn0  44800  dstregt0  45730  stoweidlem31  46474  stoweidlem59  46502  wallispilem4  46511  dirkertrigeqlem2  46542  fourierdlem43  46593  fourierdlem65  46614  catprs  49501  oppfrcl3  49620  lmdran  50161  cmdlan  50162