Theorem eqnetrrd 2994

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  eqnetrrid  3001  3netr3d  3002  cantnflem1c  9647  eqsqrt2d  15342  tanval2  16108  tanval3  16109  tanhlt1  16135  pcadd  16867  efgsres  19675  gsumval3  19844  ablfac  20027  ablsimpgfind  20049  isdrngrd  20682  isdrngrdOLD  20684  lspsneq  21039  lebnumlem3  24869  minveclem4a  25337  evthicc  25367  ioorf  25481  deg1ldgn  26005  fta1blem  26083  vieta1lem1  26225  vieta1lem2  26226  vieta1  26227  tanregt0  26455  isosctrlem2  26736  angpieqvd  26748  chordthmlem2  26750  dcubic2  26761  dquartlem1  26768  dquart  26770  asinlem  26785  atandmcj  26826  2efiatan  26835  tanatan  26836  dvatan  26852  dmgmn0  26943  dmgmdivn0  26945  lgamgulmlem2  26947  gamne0  26963  nosep1o  27600  noetasuplem4  27655  footexALT  28652  footexlem1  28653  footexlem2  28654  ttgcontlem1  28819  wlkn0  29556  nrt2irr  30409  fsuppcurry1  32655  fsuppcurry2  32656  bcm1n  32725  mxidlirred  33450  dfufd2  33528  ply1dg1rt  33555  irngnminplynz  33709  minplym1p  33710  minplynzm1p  33711  algextdeglem4  33717  constrrtll  33728  constrrtlc1  33729  constrrtcclem  33731  constrfin  33743  constrelextdg2  33744  cos9thpiminplylem2  33780  zarclssn  33870  sibfof  34338  finxpreclem2  37385  poimirlem9  37630  heicant  37656  heiborlem6  37817  lkrlspeqN  39171  cdlemg18d  40682  cdlemg21  40687  dibord  41160  lclkrlem2u  41528  lcfrlem9  41551  mapdindp4  41724  hdmaprnlem3uN  41852  hdmaprnlem9N  41858  fsuppind  42585  binomcxplemnotnn0  44352  dstregt0  45287  stoweidlem31  46036  stoweidlem59  46064  wallispilem4  46073  dirkertrigeqlem2  46104  fourierdlem43  46155  fourierdlem65  46176  catprs  49004  oppfrcl3  49123  lmdran  49664  cmdlan  49665