Theorem eqnetrrd 3028

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

Syntax hints:   → wi 4   = wceq 1508   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-9 2060  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2764  df-ne 2961

This theorem is referenced by:  syl5eqner  3035  3netr3d  3036  cantnflem1c  8942  eqsqrt2d  14587  tanval2  15344  tanval3  15345  tanhlt1  15371  pcadd  16079  efgsres  18634  efgsresOLD  18635  gsumval3  18793  ablfac  18972  isdrngrd  19263  lspsneq  19628  lebnumlem3  23285  minveclem4a  23751  evthicc  23778  ioorf  23892  deg1ldgn  24405  fta1blem  24480  vieta1lem1  24617  vieta1lem2  24618  vieta1  24619  tanregt0  24839  isosctrlem2  25113  angpieqvd  25125  chordthmlem2  25127  dcubic2  25138  dquartlem1  25145  dquart  25147  asinlem  25162  atandmcj  25203  2efiatan  25212  tanatan  25213  dvatan  25229  dmgmn0  25320  dmgmdivn0  25322  lgamgulmlem2  25324  gamne0  25340  footexALT  26221  footexlem1  26222  footexlem2  26223  ttgcontlem1  26389  wlkn0  27120  fsuppcurry1  30237  fsuppcurry2  30238  bcm1n  30291  sibfof  31275  nosep1o  32744  noetalem3  32777  finxpreclem2  34149  poimirlem9  34379  heicant  34405  heiborlem6  34573  lkrlspeqN  35789  cdlemg18d  37299  cdlemg21  37304  dibord  37777  lclkrlem2u  38145  lcfrlem9  38168  mapdindp4  38341  hdmaprnlem3uN  38469  hdmaprnlem9N  38475  ablsimpgfind  40083  binomcxplemnotnn0  40142  dstregt0  41008  stoweidlem31  41779  stoweidlem59  41807  wallispilem4  41816  dirkertrigeqlem2  41847  fourierdlem43  41898  fourierdlem65  41919