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  9640  eqsqrt2d  15335  tanval2  16101  tanval3  16102  tanhlt1  16128  pcadd  16860  efgsres  19668  gsumval3  19837  ablfac  20020  ablsimpgfind  20042  isdrngrd  20675  isdrngrdOLD  20677  lspsneq  21032  lebnumlem3  24862  minveclem4a  25330  evthicc  25360  ioorf  25474  deg1ldgn  25998  fta1blem  26076  vieta1lem1  26218  vieta1lem2  26219  vieta1  26220  tanregt0  26448  isosctrlem2  26729  angpieqvd  26741  chordthmlem2  26743  dcubic2  26754  dquartlem1  26761  dquart  26763  asinlem  26778  atandmcj  26819  2efiatan  26828  tanatan  26829  dvatan  26845  dmgmn0  26936  dmgmdivn0  26938  lgamgulmlem2  26940  gamne0  26956  nosep1o  27593  noetasuplem4  27648  footexALT  28645  footexlem1  28646  footexlem2  28647  ttgcontlem1  28812  wlkn0  29549  nrt2irr  30402  fsuppcurry1  32648  fsuppcurry2  32649  bcm1n  32718  mxidlirred  33443  dfufd2  33521  ply1dg1rt  33548  irngnminplynz  33702  minplym1p  33703  minplynzm1p  33704  algextdeglem4  33710  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrfin  33736  constrelextdg2  33737  cos9thpiminplylem2  33773  zarclssn  33863  sibfof  34331  finxpreclem2  37378  poimirlem9  37623  heicant  37649  heiborlem6  37810  lkrlspeqN  39164  cdlemg18d  40675  cdlemg21  40680  dibord  41153  lclkrlem2u  41521  lcfrlem9  41544  mapdindp4  41717  hdmaprnlem3uN  41845  hdmaprnlem9N  41851  fsuppind  42578  binomcxplemnotnn0  44345  dstregt0  45280  stoweidlem31  46029  stoweidlem59  46057  wallispilem4  46066  dirkertrigeqlem2  46097  fourierdlem43  46148  fourierdlem65  46169  catprs  49000  oppfrcl3  49119  lmdran  49660  cmdlan  49661