Theorem eqnetrrd 3008

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 3007	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ne 2940

This theorem is referenced by:  eqnetrrid  3015  3netr3d  3016  cantnflem1c  9728  eqsqrt2d  15408  tanval2  16170  tanval3  16171  tanhlt1  16197  pcadd  16928  efgsres  19757  gsumval3  19926  ablfac  20109  ablsimpgfind  20131  isdrngrd  20767  isdrngrdOLD  20769  lspsneq  21125  lebnumlem3  24996  minveclem4a  25465  evthicc  25495  ioorf  25609  deg1ldgn  26133  fta1blem  26211  vieta1lem1  26353  vieta1lem2  26354  vieta1  26355  tanregt0  26582  isosctrlem2  26863  angpieqvd  26875  chordthmlem2  26877  dcubic2  26888  dquartlem1  26895  dquart  26897  asinlem  26912  atandmcj  26953  2efiatan  26962  tanatan  26963  dvatan  26979  dmgmn0  27070  dmgmdivn0  27072  lgamgulmlem2  27074  gamne0  27090  nosep1o  27727  noetasuplem4  27782  footexALT  28727  footexlem1  28728  footexlem2  28729  ttgcontlem1  28900  wlkn0  29640  nrt2irr  30493  fsuppcurry1  32737  fsuppcurry2  32738  bcm1n  32798  mxidlirred  33501  dfufd2  33579  ply1dg1rt  33605  irngnminplynz  33756  minplym1p  33757  algextdeglem4  33762  constrrtll  33773  constrrtlc1  33774  constrrtcclem  33776  constrfin  33788  constrelextdg2  33789  zarclssn  33873  sibfof  34343  finxpreclem2  37392  poimirlem9  37637  heicant  37663  heiborlem6  37824  lkrlspeqN  39173  cdlemg18d  40684  cdlemg21  40689  dibord  41162  lclkrlem2u  41530  lcfrlem9  41553  mapdindp4  41726  hdmaprnlem3uN  41854  hdmaprnlem9N  41860  fsuppind  42605  binomcxplemnotnn0  44380  dstregt0  45298  stoweidlem31  46051  stoweidlem59  46079  wallispilem4  46088  dirkertrigeqlem2  46119  fourierdlem43  46170  fourierdlem65  46191  catprs  48915