Theorem eqnetrrd 3024

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

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

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 2733

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

This theorem is used by:  eqnetrrid  3031  3netr3d  3032  cantnflem1c  9681  eqsqrt2d  15529  tanval2  16294  tanval3  16295  tanhlt1  16321  pcadd  17060  efgsres  19945  gsumval3  20114  ablfac  20297  ablsimpgfind  20319  isdrngrd  21016  isdrngrdOLD  21018  lspsneq  21393  lebnumlem3  25277  minveclem4a  25744  evthicc  25773  ioorf  25887  deg1ldgn  26404  fta1blem  26482  vieta1lem1  26626  vieta1lem2  26627  vieta1  26628  tanregt0  26860  isosctrlem2  27140  angpieqvd  27152  chordthmlem2  27154  dcubic2  27165  dquartlem1  27172  dquart  27174  asinlem  27189  atandmcj  27230  2efiatan  27239  tanatan  27240  dvatan  27256  dmgmn0  27346  dmgmdivn0  27348  lgamgulmlem2  27350  gamne0  27366  nosep1o  28031  noetasuplem4  28086  footexALT  29186  footexlem1  29187  footexlem2  29188  dfprlng3  29419  ttgcontlem1  29455  wlkn0  30194  nrt2irr  31067  fsuppcurry1  33309  fsuppcurry2  33310  bcm1n  33380  mxidlirred  33990  dfufd2  34075  ply1dg1rt  34105  esplymhp  34193  irngnminplynz  34337  minplym1p  34338  minplynzm1p  34339  algextdeglem4  34345  constrrtll  34356  constrrtlc1  34357  constrrtcclem  34359  constrfin  34371  constrelextdg2  34372  cos9thpiminplylem2  34408  zarclssn  34498  sibfof  34965  finxpreclem2  38293  poimirlem9  38527  heicant  38553  heiborlem6  38730  lkrlspeqN  40208  cdlemg18d  41718  cdlemg21  41723  dibord  42196  lclkrlem2u  42564  lcfrlem9  42587  mapdindp4  42760  hdmaprnlem3uN  42888  hdmaprnlem9N  42894  fsuppind  43598  binomcxplemnotnn0  45325  dstregt0  46267  stoweidlem31  47010  stoweidlem59  47038  wallispilem4  47047  dirkertrigeqlem2  47078  fourierdlem43  47129  fourierdlem65  47150  catprs  50088  oppfrcl3  50207  lmdran  50748  cmdlan  50749