Theorem eqnetrrd 3010

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  eqnetrrid  3017  3netr3d  3018  cantnflem1c  9682  eqsqrt2d  15315  tanval2  16076  tanval3  16077  tanhlt1  16103  pcadd  16822  efgsres  19606  gsumval3  19775  ablfac  19958  ablsimpgfind  19980  isdrngrd  20391  isdrngrdOLD  20393  lspsneq  20735  lebnumlem3  24479  minveclem4a  24947  evthicc  24976  ioorf  25090  deg1ldgn  25611  fta1blem  25686  vieta1lem1  25823  vieta1lem2  25824  vieta1  25825  tanregt0  26048  isosctrlem2  26324  angpieqvd  26336  chordthmlem2  26338  dcubic2  26349  dquartlem1  26356  dquart  26358  asinlem  26373  atandmcj  26414  2efiatan  26423  tanatan  26424  dvatan  26440  dmgmn0  26530  dmgmdivn0  26532  lgamgulmlem2  26534  gamne0  26550  nosep1o  27184  noetasuplem4  27239  footexALT  27969  footexlem1  27970  footexlem2  27971  ttgcontlem1  28142  wlkn0  28878  nrt2irr  29726  fsuppcurry1  31950  fsuppcurry2  31951  bcm1n  32006  mxidlirred  32588  irngnminplynz  32771  algextdeglem1  32772  zarclssn  32853  sibfof  33339  finxpreclem2  36271  poimirlem9  36497  heicant  36523  heiborlem6  36684  lkrlspeqN  38041  cdlemg18d  39552  cdlemg21  39557  dibord  40030  lclkrlem2u  40398  lcfrlem9  40421  mapdindp4  40594  hdmaprnlem3uN  40722  hdmaprnlem9N  40728  fsuppind  41162  binomcxplemnotnn0  43115  dstregt0  43991  stoweidlem31  44747  stoweidlem59  44775  wallispilem4  44784  dirkertrigeqlem2  44815  fourierdlem43  44866  fourierdlem65  44887  catprs  47631