Theorem eqnetrrd 3023

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ne 2956

This theorem is used by:  eqnetrrid  3030  3netr3d  3031  cantnflem1c  9666  eqsqrt2d  15456  tanval2  16221  tanval3  16222  tanhlt1  16248  pcadd  16981  efgsres  19865  gsumval3  20034  ablfac  20217  ablsimpgfind  20239  isdrngrd  20932  isdrngrdOLD  20934  lspsneq  21309  lebnumlem3  25191  minveclem4a  25658  evthicc  25687  ioorf  25801  deg1ldgn  26318  fta1blem  26396  vieta1lem1  26542  vieta1lem2  26543  vieta1  26544  tanregt0  26776  isosctrlem2  27056  angpieqvd  27068  chordthmlem2  27070  dcubic2  27081  dquartlem1  27088  dquart  27090  asinlem  27105  atandmcj  27146  2efiatan  27155  tanatan  27156  dvatan  27172  dmgmn0  27262  dmgmdivn0  27264  lgamgulmlem2  27266  gamne0  27282  nosep1o  27917  noetasuplem4  27972  footexALT  29072  footexlem1  29073  footexlem2  29074  dfprlng3  29305  ttgcontlem1  29341  wlkn0  30080  nrt2irr  30953  fsuppcurry1  33195  fsuppcurry2  33196  bcm1n  33266  mxidlirred  33875  dfufd2  33960  ply1dg1rt  33990  esplymhp  34078  irngnminplynz  34222  minplym1p  34223  minplynzm1p  34224  algextdeglem4  34230  constrrtll  34241  constrrtlc1  34242  constrrtcclem  34244  constrfin  34256  constrelextdg2  34257  cos9thpiminplylem2  34293  zarclssn  34383  sibfof  34851  finxpreclem2  38144  poimirlem9  38378  heicant  38404  heiborlem6  38566  lkrlspeqN  40044  cdlemg18d  41554  cdlemg21  41559  dibord  42032  lclkrlem2u  42400  lcfrlem9  42423  mapdindp4  42596  hdmaprnlem3uN  42724  hdmaprnlem9N  42730  fsuppind  43436  binomcxplemnotnn0  45180  dstregt0  46115  stoweidlem31  46859  stoweidlem59  46887  wallispilem4  46896  dirkertrigeqlem2  46927  fourierdlem43  46978  fourierdlem65  46999  catprs  49937  oppfrcl3  50056  lmdran  50597  cmdlan  50598