Theorem eqnetrrd 3025

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

Syntax hints:   → wi 4   = wceq 1560   ≠ wne 2957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ne 2958

This theorem is referenced by:  eqnetrrid  3032  3netr3d  3033  cantnflem1c  9642  eqsqrt2d  15396  tanval2  16165  tanval3  16166  tanhlt1  16192  pcadd  16925  efgsres  19778  gsumval3  19947  ablfac  20130  ablsimpgfind  20152  isdrngrd  20812  isdrngrdOLD  20814  lspsneq  21189  lebnumlem3  25022  minveclem4a  25489  evthicc  25518  ioorf  25632  deg1ldgn  26150  fta1blem  26228  vieta1lem1  26371  vieta1lem2  26372  vieta1  26373  tanregt0  26601  isosctrlem2  26881  angpieqvd  26893  chordthmlem2  26895  dcubic2  26906  dquartlem1  26913  dquart  26915  asinlem  26930  atandmcj  26971  2efiatan  26980  tanatan  26981  dvatan  26997  dmgmn0  27087  dmgmdivn0  27089  lgamgulmlem2  27091  gamne0  27107  nosep1o  27742  noetasuplem4  27797  footexALT  28888  footexlem1  28889  footexlem2  28890  ttgcontlem1  29082  wlkn0  29818  nrt2irr  30672  fsuppcurry1  32923  fsuppcurry2  32924  bcm1n  32994  mxidlirred  33657  dfufd2  33743  ply1dg1rt  33773  esplymhp  33862  irngnminplynz  34006  minplym1p  34007  minplynzm1p  34008  algextdeglem4  34014  constrrtll  34025  constrrtlc1  34026  constrrtcclem  34028  constrfin  34040  constrelextdg2  34041  cos9thpiminplylem2  34077  zarclssn  34167  sibfof  34634  finxpreclem2  37881  poimirlem9  38125  heicant  38151  heiborlem6  38312  lkrlspeqN  39792  cdlemg18d  41302  cdlemg21  41307  dibord  41780  lclkrlem2u  42148  lcfrlem9  42171  mapdindp4  42344  hdmaprnlem3uN  42472  hdmaprnlem9N  42478  fsuppind  43169  binomcxplemnotnn0  44929  dstregt0  45858  stoweidlem31  46602  stoweidlem59  46630  wallispilem4  46639  dirkertrigeqlem2  46670  fourierdlem43  46721  fourierdlem65  46742  catprs  49629  oppfrcl3  49748  lmdran  50289  cmdlan  50290