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 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  eqnetrrid  3030  3netr3d  3031  cantnflem1c  9695  eqsqrt2d  15545  tanval2  16310  tanval3  16311  tanhlt1  16337  pcadd  17076  efgsres  19961  gsumval3  20130  ablfac  20313  ablsimpgfind  20335  isdrngrd  21032  isdrngrdOLD  21034  lspsneq  21409  lebnumlem3  25293  minveclem4a  25760  evthicc  25789  ioorf  25903  deg1ldgn  26420  fta1blem  26498  vieta1lem1  26642  vieta1lem2  26643  vieta1  26644  tanregt0  26876  isosctrlem2  27156  angpieqvd  27168  chordthmlem2  27170  dcubic2  27181  dquartlem1  27188  dquart  27190  asinlem  27205  atandmcj  27246  2efiatan  27255  tanatan  27256  dvatan  27272  dmgmn0  27362  dmgmdivn0  27364  lgamgulmlem2  27366  gamne0  27382  nosep1o  28047  noetasuplem4  28102  footexALT  29202  footexlem1  29203  footexlem2  29204  dfprlng3  29435  ttgcontlem1  29471  wlkn0  30210  nrt2irr  31083  fsuppcurry1  33366  fsuppcurry2  33367  bcm1n  33437  mxidlirred  34047  dfufd2  34132  ply1dg1rt  34162  esplymhp  34250  irngnminplynz  34394  minplym1p  34395  minplynzm1p  34396  algextdeglem4  34402  constrrtll  34413  constrrtlc1  34414  constrrtcclem  34416  constrfin  34428  constrelextdg2  34429  cos9thpiminplylem2  34465  zarclssn  34555  sibfof  35022  finxpreclem2  38422  poimirlem9  38656  heicant  38682  heiborlem6  38859  lkrlspeqN  40337  cdlemg18d  41847  cdlemg21  41852  dibord  42325  lclkrlem2u  42693  lcfrlem9  42716  mapdindp4  42889  hdmaprnlem3uN  43017  hdmaprnlem9N  43023  fsuppind  43727  binomcxplemnotnn0  45449  dstregt0  46406  stoweidlem31  47149  stoweidlem59  47177  wallispilem4  47186  dirkertrigeqlem2  47217  fourierdlem43  47268  fourierdlem65  47289  catprs  50233  oppfrcl3  50354  lmdran  50962  cmdlan  50963