Theorem eqnetrrd 3013

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 3012	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-ne 2945

This theorem is referenced by:  eqnetrrid  3020  3netr3d  3021  cantnflem1c  9406  eqsqrt2d  15061  tanval2  15823  tanval3  15824  tanhlt1  15850  pcadd  16571  efgsres  19325  gsumval3  19489  ablfac  19672  ablsimpgfind  19694  isdrngrd  19998  lspsneq  20365  lebnumlem3  24107  minveclem4a  24575  evthicc  24604  ioorf  24718  deg1ldgn  25239  fta1blem  25314  vieta1lem1  25451  vieta1lem2  25452  vieta1  25453  tanregt0  25676  isosctrlem2  25950  angpieqvd  25962  chordthmlem2  25964  dcubic2  25975  dquartlem1  25982  dquart  25984  asinlem  25999  atandmcj  26040  2efiatan  26049  tanatan  26050  dvatan  26066  dmgmn0  26156  dmgmdivn0  26158  lgamgulmlem2  26160  gamne0  26176  footexALT  27060  footexlem1  27061  footexlem2  27062  ttgcontlem1  27233  wlkn0  27968  fsuppcurry1  31039  fsuppcurry2  31040  bcm1n  31095  zarclssn  31802  sibfof  32286  nosep1o  33863  noetasuplem4  33918  finxpreclem2  35540  poimirlem9  35765  heicant  35791  heiborlem6  35953  lkrlspeqN  37164  cdlemg18d  38674  cdlemg21  38679  dibord  39152  lclkrlem2u  39520  lcfrlem9  39543  mapdindp4  39716  hdmaprnlem3uN  39844  hdmaprnlem9N  39850  fsuppind  40259  binomcxplemnotnn0  41927  dstregt0  42773  stoweidlem31  43526  stoweidlem59  43554  wallispilem4  43563  dirkertrigeqlem2  43594  fourierdlem43  43645  fourierdlem65  43666  catprs  46244