Theorem eqnetrrd 2993

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetrrid  3000  3netr3d  3001  cantnflem1c  9583  eqsqrt2d  15276  tanval2  16042  tanval3  16043  tanhlt1  16069  pcadd  16801  efgsres  19617  gsumval3  19786  ablfac  19969  ablsimpgfind  19991  isdrngrd  20651  isdrngrdOLD  20653  lspsneq  21029  lebnumlem3  24860  minveclem4a  25328  evthicc  25358  ioorf  25472  deg1ldgn  25996  fta1blem  26074  vieta1lem1  26216  vieta1lem2  26217  vieta1  26218  tanregt0  26446  isosctrlem2  26727  angpieqvd  26739  chordthmlem2  26741  dcubic2  26752  dquartlem1  26759  dquart  26761  asinlem  26776  atandmcj  26817  2efiatan  26826  tanatan  26827  dvatan  26843  dmgmn0  26934  dmgmdivn0  26936  lgamgulmlem2  26938  gamne0  26954  nosep1o  27591  noetasuplem4  27646  footexALT  28663  footexlem1  28664  footexlem2  28665  ttgcontlem1  28830  wlkn0  29566  nrt2irr  30417  fsuppcurry1  32668  fsuppcurry2  32669  bcm1n  32738  mxidlirred  33409  dfufd2  33487  ply1dg1rt  33515  irngnminplynz  33679  minplym1p  33680  minplynzm1p  33681  algextdeglem4  33687  constrrtll  33698  constrrtlc1  33699  constrrtcclem  33701  constrfin  33713  constrelextdg2  33714  cos9thpiminplylem2  33750  zarclssn  33840  sibfof  34308  finxpreclem2  37364  poimirlem9  37609  heicant  37635  heiborlem6  37796  lkrlspeqN  39150  cdlemg18d  40660  cdlemg21  40665  dibord  41138  lclkrlem2u  41506  lcfrlem9  41529  mapdindp4  41702  hdmaprnlem3uN  41830  hdmaprnlem9N  41836  fsuppind  42563  binomcxplemnotnn0  44329  dstregt0  45264  stoweidlem31  46012  stoweidlem59  46040  wallispilem4  46049  dirkertrigeqlem2  46080  fourierdlem43  46131  fourierdlem65  46152  catprs  48996  oppfrcl3  49115  lmdran  49656  cmdlan  49657