Theorem eqnetrrd 2996

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  eqnetrrid  3003  3netr3d  3004  cantnflem1c  9577  eqsqrt2d  15276  tanval2  16042  tanval3  16043  tanhlt1  16069  pcadd  16801  efgsres  19650  gsumval3  19819  ablfac  20002  ablsimpgfind  20024  isdrngrd  20681  isdrngrdOLD  20683  lspsneq  21059  lebnumlem3  24889  minveclem4a  25357  evthicc  25387  ioorf  25501  deg1ldgn  26025  fta1blem  26103  vieta1lem1  26245  vieta1lem2  26246  vieta1  26247  tanregt0  26475  isosctrlem2  26756  angpieqvd  26768  chordthmlem2  26770  dcubic2  26781  dquartlem1  26788  dquart  26790  asinlem  26805  atandmcj  26846  2efiatan  26855  tanatan  26856  dvatan  26872  dmgmn0  26963  dmgmdivn0  26965  lgamgulmlem2  26967  gamne0  26983  nosep1o  27620  noetasuplem4  27675  footexALT  28696  footexlem1  28697  footexlem2  28698  ttgcontlem1  28863  wlkn0  29599  nrt2irr  30453  fsuppcurry1  32707  fsuppcurry2  32708  bcm1n  32777  mxidlirred  33437  dfufd2  33515  ply1dg1rt  33543  esplymhp  33589  irngnminplynz  33725  minplym1p  33726  minplynzm1p  33727  algextdeglem4  33733  constrrtll  33744  constrrtlc1  33745  constrrtcclem  33747  constrfin  33759  constrelextdg2  33760  cos9thpiminplylem2  33796  zarclssn  33886  sibfof  34353  finxpreclem2  37432  poimirlem9  37677  heicant  37703  heiborlem6  37864  lkrlspeqN  39218  cdlemg18d  40728  cdlemg21  40733  dibord  41206  lclkrlem2u  41574  lcfrlem9  41597  mapdindp4  41770  hdmaprnlem3uN  41898  hdmaprnlem9N  41904  fsuppind  42631  binomcxplemnotnn0  44397  dstregt0  45331  stoweidlem31  46077  stoweidlem59  46105  wallispilem4  46114  dirkertrigeqlem2  46145  fourierdlem43  46196  fourierdlem65  46217  catprs  49051  oppfrcl3  49170  lmdran  49711  cmdlan  49712