Theorem eqnetrrd 3007

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

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

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  eqnetrrid  3014  3netr3d  3015  cantnflem1c  9684  eqsqrt2d  15319  tanval2  16080  tanval3  16081  tanhlt1  16107  pcadd  16826  efgsres  19647  gsumval3  19816  ablfac  19999  ablsimpgfind  20021  isdrngrd  20534  isdrngrdOLD  20536  lspsneq  20880  lebnumlem3  24709  minveclem4a  25178  evthicc  25208  ioorf  25322  deg1ldgn  25846  fta1blem  25921  vieta1lem1  26059  vieta1lem2  26060  vieta1  26061  tanregt0  26284  isosctrlem2  26560  angpieqvd  26572  chordthmlem2  26574  dcubic2  26585  dquartlem1  26592  dquart  26594  asinlem  26609  atandmcj  26650  2efiatan  26659  tanatan  26660  dvatan  26676  dmgmn0  26766  dmgmdivn0  26768  lgamgulmlem2  26770  gamne0  26786  nosep1o  27420  noetasuplem4  27475  footexALT  28236  footexlem1  28237  footexlem2  28238  ttgcontlem1  28409  wlkn0  29145  nrt2irr  29993  fsuppcurry1  32217  fsuppcurry2  32218  bcm1n  32273  mxidlirred  32862  irngnminplynz  33060  minplym1p  33061  algextdeglem4  33065  zarclssn  33151  sibfof  33637  finxpreclem2  36574  poimirlem9  36800  heicant  36826  heiborlem6  36987  lkrlspeqN  38344  cdlemg18d  39855  cdlemg21  39860  dibord  40333  lclkrlem2u  40701  lcfrlem9  40724  mapdindp4  40897  hdmaprnlem3uN  41025  hdmaprnlem9N  41031  fsuppind  41464  binomcxplemnotnn0  43417  dstregt0  44289  stoweidlem31  45045  stoweidlem59  45073  wallispilem4  45082  dirkertrigeqlem2  45113  fourierdlem43  45164  fourierdlem65  45185  catprs  47718