Theorem eqnetrrd 3032

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  eqnetrrid  3039  3netr3d  3040  cantnflem1c  9655  eqsqrt2d  15419  tanval2  16188  tanval3  16189  tanhlt1  16215  pcadd  16948  efgsres  19807  gsumval3  19976  ablfac  20159  ablsimpgfind  20181  isdrngrd  20847  isdrngrdOLD  20849  lspsneq  21223  lebnumlem3  25090  minveclem4a  25557  evthicc  25586  ioorf  25700  deg1ldgn  26218  fta1blem  26296  vieta1lem1  26439  vieta1lem2  26440  vieta1  26441  tanregt0  26669  isosctrlem2  26949  angpieqvd  26961  chordthmlem2  26963  dcubic2  26974  dquartlem1  26981  dquart  26983  asinlem  26998  atandmcj  27039  2efiatan  27048  tanatan  27049  dvatan  27065  dmgmn0  27155  dmgmdivn0  27157  lgamgulmlem2  27159  gamne0  27175  nosep1o  27810  noetasuplem4  27865  footexALT  28956  footexlem1  28957  footexlem2  28958  ttgcontlem1  29174  wlkn0  29910  nrt2irr  30764  fsuppcurry1  33009  fsuppcurry2  33010  bcm1n  33080  mxidlirred  33699  dfufd2  33784  ply1dg1rt  33814  esplymhp  33902  irngnminplynz  34046  minplym1p  34047  minplynzm1p  34048  algextdeglem4  34054  constrrtll  34065  constrrtlc1  34066  constrrtcclem  34068  constrfin  34080  constrelextdg2  34081  cos9thpiminplylem2  34117  zarclssn  34207  sibfof  34674  finxpreclem2  37923  poimirlem9  38167  heicant  38193  heiborlem6  38354  lkrlspeqN  39834  cdlemg18d  41344  cdlemg21  41349  dibord  41822  lclkrlem2u  42190  lcfrlem9  42213  mapdindp4  42386  hdmaprnlem3uN  42514  hdmaprnlem9N  42520  fsuppind  43213  binomcxplemnotnn0  44957  dstregt0  45892  stoweidlem31  46636  stoweidlem59  46664  wallispilem4  46673  dirkertrigeqlem2  46704  fourierdlem43  46755  fourierdlem65  46776  catprs  49673  oppfrcl3  49792  lmdran  50333  cmdlan  50334