Theorem eqnetrrd 3084

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

Syntax hints:   → wi 4   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  eqnetrrid  3091  3netr3d  3092  cantnflem1c  9144  eqsqrt2d  14722  tanval2  15480  tanval3  15481  tanhlt1  15507  pcadd  16219  efgsres  18858  gsumval3  19021  ablfac  19204  ablsimpgfind  19226  isdrngrd  19522  lspsneq  19888  lebnumlem3  23561  minveclem4a  24027  evthicc  24054  ioorf  24168  deg1ldgn  24681  fta1blem  24756  vieta1lem1  24893  vieta1lem2  24894  vieta1  24895  tanregt0  25117  isosctrlem2  25391  angpieqvd  25403  chordthmlem2  25405  dcubic2  25416  dquartlem1  25423  dquart  25425  asinlem  25440  atandmcj  25481  2efiatan  25490  tanatan  25491  dvatan  25507  dmgmn0  25597  dmgmdivn0  25599  lgamgulmlem2  25601  gamne0  25617  footexALT  26498  footexlem1  26499  footexlem2  26500  ttgcontlem1  26665  wlkn0  27396  fsuppcurry1  30455  fsuppcurry2  30456  bcm1n  30512  sibfof  31593  nosep1o  33181  noetalem3  33214  finxpreclem2  34665  poimirlem9  34895  heicant  34921  heiborlem6  35088  lkrlspeqN  36301  cdlemg18d  37811  cdlemg21  37816  dibord  38289  lclkrlem2u  38657  lcfrlem9  38680  mapdindp4  38853  hdmaprnlem3uN  38981  hdmaprnlem9N  38987  binomcxplemnotnn0  40681  dstregt0  41540  stoweidlem31  42310  stoweidlem59  42338  wallispilem4  42347  dirkertrigeqlem2  42378  fourierdlem43  42429  fourierdlem65  42450