Theorem eqnetrrd 3006

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 3005	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  eqnetrrid  3013  3netr3d  3014  cantnflem1c  9724  eqsqrt2d  15403  tanval2  16165  tanval3  16166  tanhlt1  16192  pcadd  16922  efgsres  19770  gsumval3  19939  ablfac  20122  ablsimpgfind  20144  isdrngrd  20782  isdrngrdOLD  20784  lspsneq  21141  lebnumlem3  25008  minveclem4a  25477  evthicc  25507  ioorf  25621  deg1ldgn  26146  fta1blem  26224  vieta1lem1  26366  vieta1lem2  26367  vieta1  26368  tanregt0  26595  isosctrlem2  26876  angpieqvd  26888  chordthmlem2  26890  dcubic2  26901  dquartlem1  26908  dquart  26910  asinlem  26925  atandmcj  26966  2efiatan  26975  tanatan  26976  dvatan  26992  dmgmn0  27083  dmgmdivn0  27085  lgamgulmlem2  27087  gamne0  27103  nosep1o  27740  noetasuplem4  27795  footexALT  28740  footexlem1  28741  footexlem2  28742  ttgcontlem1  28913  wlkn0  29653  nrt2irr  30501  fsuppcurry1  32742  fsuppcurry2  32743  bcm1n  32802  mxidlirred  33479  dfufd2  33557  ply1dg1rt  33583  irngnminplynz  33719  minplym1p  33720  algextdeglem4  33725  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrfin  33750  constrelextdg2  33751  zarclssn  33833  sibfof  34321  finxpreclem2  37372  poimirlem9  37615  heicant  37641  heiborlem6  37802  lkrlspeqN  39152  cdlemg18d  40663  cdlemg21  40668  dibord  41141  lclkrlem2u  41509  lcfrlem9  41532  mapdindp4  41705  hdmaprnlem3uN  41833  hdmaprnlem9N  41839  fsuppind  42576  binomcxplemnotnn0  44351  dstregt0  45231  stoweidlem31  45986  stoweidlem59  46014  wallispilem4  46023  dirkertrigeqlem2  46054  fourierdlem43  46105  fourierdlem65  46126  catprs  48799