Theorem eqnetrrd 3026

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  eqnetrrid  3033  3netr3d  3034  cantnflem1c  9652  eqsqrt2d  15416  tanval2  16184  tanval3  16185  tanhlt1  16211  pcadd  16944  efgsres  19803  gsumval3  19972  ablfac  20155  ablsimpgfind  20177  isdrngrd  20869  isdrngrdOLD  20871  lspsneq  21246  lebnumlem3  25122  minveclem4a  25589  evthicc  25618  ioorf  25732  deg1ldgn  26250  fta1blem  26328  vieta1lem1  26471  vieta1lem2  26472  vieta1  26473  tanregt0  26704  isosctrlem2  26984  angpieqvd  26996  chordthmlem2  26998  dcubic2  27009  dquartlem1  27016  dquart  27018  asinlem  27033  atandmcj  27074  2efiatan  27083  tanatan  27084  dvatan  27100  dmgmn0  27190  dmgmdivn0  27192  lgamgulmlem2  27194  gamne0  27210  nosep1o  27845  noetasuplem4  27900  footexALT  28998  footexlem1  28999  footexlem2  29000  dfprlng3  29198  ttgcontlem1  29234  wlkn0  29970  nrt2irr  30824  fsuppcurry1  33069  fsuppcurry2  33070  bcm1n  33140  mxidlirred  33755  dfufd2  33840  ply1dg1rt  33870  esplymhp  33958  irngnminplynz  34102  minplym1p  34103  minplynzm1p  34104  algextdeglem4  34110  constrrtll  34121  constrrtlc1  34122  constrrtcclem  34124  constrfin  34136  constrelextdg2  34137  cos9thpiminplylem2  34173  zarclssn  34263  sibfof  34730  finxpreclem2  38036  poimirlem9  38280  heicant  38306  heiborlem6  38467  lkrlspeqN  39945  cdlemg18d  41455  cdlemg21  41460  dibord  41933  lclkrlem2u  42301  lcfrlem9  42324  mapdindp4  42497  hdmaprnlem3uN  42625  hdmaprnlem9N  42631  fsuppind  43322  binomcxplemnotnn0  45066  dstregt0  46001  stoweidlem31  46745  stoweidlem59  46773  wallispilem4  46782  dirkertrigeqlem2  46813  fourierdlem43  46864  fourierdlem65  46885  catprs  49789  oppfrcl3  49908  lmdran  50449  cmdlan  50450