Theorem eqnetrrd 2850

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

Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  syl5eqner  2857  3netr3d  2858  cantnflem1c  8467  eqsqrt2d  13956  tanval2  14702  tanval3  14703  tanhlt1  14729  pcadd  15431  efgsres  17974  gsumval3  18131  ablfac  18310  isdrngrd  18596  lspsneq  18943  lebnumlem3  22570  minveclem4a  23009  evthicc  23035  ioorf  23147  deg1ldgn  23657  fta1blem  23732  vieta1lem1  23869  vieta1lem2  23870  vieta1  23871  tanregt0  24089  isosctrlem2  24349  angpieqvd  24358  chordthmlem2  24360  dcubic2  24371  dquartlem1  24378  dquart  24380  asinlem  24395  atandmcj  24436  2efiatan  24445  tanatan  24446  dvatan  24462  dmgmn0  24552  dmgmdivn0  24554  lgamgulmlem2  24556  gamne0  24572  footex  25413  ttgcontlem1  25565  eupath2lem3  26506  bcm1n  28941  sibfof  29729  finxpreclem2  32403  poimirlem9  32588  heicant  32614  heiborlem6  32785  lkrlspeqN  33476  cdlemg18d  34987  cdlemg21  34992  dibord  35466  lclkrlem2u  35834  lcfrlem9  35857  mapdindp4  36030  hdmaprnlem3uN  36161  hdmaprnlem9N  36167  binomcxplemnotnn0  37577  dstregt0  38434  stoweidlem31  38924  stoweidlem59  38952  wallispilem4  38961  dirkertrigeqlem2  38992  fourierdlem43  39043  fourierdlem65  39064  1wlkn0  40825