Theorem eqnetrrd 2998

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ne 2931

This theorem is referenced by:  eqnetrrid  3005  3netr3d  3006  cantnflem1c  9594  eqsqrt2d  15290  tanval2  16056  tanval3  16057  tanhlt1  16083  pcadd  16815  efgsres  19665  gsumval3  19834  ablfac  20017  ablsimpgfind  20039  isdrngrd  20697  isdrngrdOLD  20699  lspsneq  21075  lebnumlem3  24916  minveclem4a  25384  evthicc  25414  ioorf  25528  deg1ldgn  26052  fta1blem  26130  vieta1lem1  26272  vieta1lem2  26273  vieta1  26274  tanregt0  26502  isosctrlem2  26783  angpieqvd  26795  chordthmlem2  26797  dcubic2  26808  dquartlem1  26815  dquart  26817  asinlem  26832  atandmcj  26873  2efiatan  26882  tanatan  26883  dvatan  26899  dmgmn0  26990  dmgmdivn0  26992  lgamgulmlem2  26994  gamne0  27010  nosep1o  27647  noetasuplem4  27702  footexALT  28739  footexlem1  28740  footexlem2  28741  ttgcontlem1  28906  wlkn0  29643  nrt2irr  30497  fsuppcurry1  32752  fsuppcurry2  32753  bcm1n  32824  mxidlirred  33502  dfufd2  33580  ply1dg1rt  33610  esplymhp  33675  irngnminplynz  33818  minplym1p  33819  minplynzm1p  33820  algextdeglem4  33826  constrrtll  33837  constrrtlc1  33838  constrrtcclem  33840  constrfin  33852  constrelextdg2  33853  cos9thpiminplylem2  33889  zarclssn  33979  sibfof  34446  finxpreclem2  37534  poimirlem9  37769  heicant  37795  heiborlem6  37956  lkrlspeqN  39370  cdlemg18d  40880  cdlemg21  40885  dibord  41358  lclkrlem2u  41726  lcfrlem9  41749  mapdindp4  41922  hdmaprnlem3uN  42050  hdmaprnlem9N  42056  fsuppind  42775  binomcxplemnotnn0  44539  dstregt0  45472  stoweidlem31  46217  stoweidlem59  46245  wallispilem4  46254  dirkertrigeqlem2  46285  fourierdlem43  46336  fourierdlem65  46357  catprs  49198  oppfrcl3  49317  lmdran  49858  cmdlan  49859