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  9688  eqsqrt2d  15536  tanval2  16301  tanval3  16302  tanhlt1  16328  pcadd  17067  efgsres  19952  gsumval3  20121  ablfac  20304  ablsimpgfind  20326  isdrngrd  21023  isdrngrdOLD  21025  lspsneq  21400  lebnumlem3  25284  minveclem4a  25751  evthicc  25780  ioorf  25894  deg1ldgn  26411  fta1blem  26489  vieta1lem1  26633  vieta1lem2  26634  vieta1  26635  tanregt0  26867  isosctrlem2  27147  angpieqvd  27159  chordthmlem2  27161  dcubic2  27172  dquartlem1  27179  dquart  27181  asinlem  27196  atandmcj  27237  2efiatan  27246  tanatan  27247  dvatan  27263  dmgmn0  27353  dmgmdivn0  27355  lgamgulmlem2  27357  gamne0  27373  nosep1o  28038  noetasuplem4  28093  footexALT  29193  footexlem1  29194  footexlem2  29195  dfprlng3  29426  ttgcontlem1  29462  wlkn0  30201  nrt2irr  31074  fsuppcurry1  33316  fsuppcurry2  33317  bcm1n  33387  mxidlirred  33997  dfufd2  34082  ply1dg1rt  34112  esplymhp  34200  irngnminplynz  34344  minplym1p  34345  minplynzm1p  34346  algextdeglem4  34352  constrrtll  34363  constrrtlc1  34364  constrrtcclem  34366  constrfin  34378  constrelextdg2  34379  cos9thpiminplylem2  34415  zarclssn  34505  sibfof  34972  finxpreclem2  38313  poimirlem9  38547  heicant  38573  heiborlem6  38750  lkrlspeqN  40228  cdlemg18d  41738  cdlemg21  41743  dibord  42216  lclkrlem2u  42584  lcfrlem9  42607  mapdindp4  42780  hdmaprnlem3uN  42908  hdmaprnlem9N  42914  fsuppind  43618  binomcxplemnotnn0  45339  dstregt0  46297  stoweidlem31  47040  stoweidlem59  47068  wallispilem4  47077  dirkertrigeqlem2  47108  fourierdlem43  47159  fourierdlem65  47180  catprs  50118  oppfrcl3  50237  lmdran  50778  cmdlan  50779