Theorem eqnetrrd 3028

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  eqnetrrid  3035  3netr3d  3036  cantnflem1c  9663  eqsqrt2d  15444  tanval2  16211  tanval3  16212  tanhlt1  16238  pcadd  16971  efgsres  19852  gsumval3  20021  ablfac  20204  ablsimpgfind  20226  isdrngrd  20919  isdrngrdOLD  20921  lspsneq  21296  lebnumlem3  25173  minveclem4a  25640  evthicc  25669  ioorf  25783  deg1ldgn  26301  fta1blem  26379  vieta1lem1  26522  vieta1lem2  26523  vieta1  26524  tanregt0  26755  isosctrlem2  27035  angpieqvd  27047  chordthmlem2  27049  dcubic2  27060  dquartlem1  27067  dquart  27069  asinlem  27084  atandmcj  27125  2efiatan  27134  tanatan  27135  dvatan  27151  dmgmn0  27241  dmgmdivn0  27243  lgamgulmlem2  27245  gamne0  27261  nosep1o  27896  noetasuplem4  27951  footexALT  29049  footexlem1  29050  footexlem2  29051  dfprlng3  29253  ttgcontlem1  29289  wlkn0  30028  nrt2irr  30895  fsuppcurry1  33139  fsuppcurry2  33140  bcm1n  33210  mxidlirred  33819  dfufd2  33904  ply1dg1rt  33934  esplymhp  34022  irngnminplynz  34166  minplym1p  34167  minplynzm1p  34168  algextdeglem4  34174  constrrtll  34185  constrrtlc1  34186  constrrtcclem  34188  constrfin  34200  constrelextdg2  34201  cos9thpiminplylem2  34237  zarclssn  34327  sibfof  34795  finxpreclem2  38093  poimirlem9  38337  heicant  38363  heiborlem6  38525  lkrlspeqN  40003  cdlemg18d  41513  cdlemg21  41518  dibord  41991  lclkrlem2u  42359  lcfrlem9  42382  mapdindp4  42555  hdmaprnlem3uN  42683  hdmaprnlem9N  42689  fsuppind  43380  binomcxplemnotnn0  45124  dstregt0  46059  stoweidlem31  46803  stoweidlem59  46831  wallispilem4  46840  dirkertrigeqlem2  46871  fourierdlem43  46922  fourierdlem65  46943  catprs  49846  oppfrcl3  49965  lmdran  50506  cmdlan  50507