Theorem eqnetrrd 3000

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

Syntax hints:   → wi 4   = wceq 1543   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ne 2933

This theorem is referenced by:  eqnetrrid  3007  3netr3d  3008  cantnflem1c  9280  eqsqrt2d  14897  tanval2  15657  tanval3  15658  tanhlt1  15684  pcadd  16405  efgsres  19082  gsumval3  19246  ablfac  19429  ablsimpgfind  19451  isdrngrd  19747  lspsneq  20113  lebnumlem3  23814  minveclem4a  24281  evthicc  24310  ioorf  24424  deg1ldgn  24945  fta1blem  25020  vieta1lem1  25157  vieta1lem2  25158  vieta1  25159  tanregt0  25382  isosctrlem2  25656  angpieqvd  25668  chordthmlem2  25670  dcubic2  25681  dquartlem1  25688  dquart  25690  asinlem  25705  atandmcj  25746  2efiatan  25755  tanatan  25756  dvatan  25772  dmgmn0  25862  dmgmdivn0  25864  lgamgulmlem2  25866  gamne0  25882  footexALT  26763  footexlem1  26764  footexlem2  26765  ttgcontlem1  26930  wlkn0  27662  fsuppcurry1  30734  fsuppcurry2  30735  bcm1n  30790  zarclssn  31491  sibfof  31973  nosep1o  33570  noetasuplem4  33625  finxpreclem2  35247  poimirlem9  35472  heicant  35498  heiborlem6  35660  lkrlspeqN  36871  cdlemg18d  38381  cdlemg21  38386  dibord  38859  lclkrlem2u  39227  lcfrlem9  39250  mapdindp4  39423  hdmaprnlem3uN  39551  hdmaprnlem9N  39557  fsuppind  39930  binomcxplemnotnn0  41588  dstregt0  42433  stoweidlem31  43190  stoweidlem59  43218  wallispilem4  43227  dirkertrigeqlem2  43258  fourierdlem43  43309  fourierdlem65  43330  catprs  45908