Theorem eqnetrrd 3004

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

Syntax hints:   → wi 4   = wceq 1534   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-ne 2936

This theorem is referenced by:  eqnetrrid  3011  3netr3d  3012  cantnflem1c  9702  eqsqrt2d  15339  tanval2  16101  tanval3  16102  tanhlt1  16128  pcadd  16849  efgsres  19684  gsumval3  19853  ablfac  20036  ablsimpgfind  20058  isdrngrd  20647  isdrngrdOLD  20649  lspsneq  20999  lebnumlem3  24876  minveclem4a  25345  evthicc  25375  ioorf  25489  deg1ldgn  26016  fta1blem  26092  vieta1lem1  26232  vieta1lem2  26233  vieta1  26234  tanregt0  26460  isosctrlem2  26738  angpieqvd  26750  chordthmlem2  26752  dcubic2  26763  dquartlem1  26770  dquart  26772  asinlem  26787  atandmcj  26828  2efiatan  26837  tanatan  26838  dvatan  26854  dmgmn0  26945  dmgmdivn0  26947  lgamgulmlem2  26949  gamne0  26965  nosep1o  27601  noetasuplem4  27656  footexALT  28509  footexlem1  28510  footexlem2  28511  ttgcontlem1  28682  wlkn0  29422  nrt2irr  30270  fsuppcurry1  32491  fsuppcurry2  32492  bcm1n  32547  mxidlirred  33121  irngnminplynz  33318  minplym1p  33319  algextdeglem4  33324  zarclssn  33410  sibfof  33896  finxpreclem2  36805  poimirlem9  37037  heicant  37063  heiborlem6  37224  lkrlspeqN  38580  cdlemg18d  40091  cdlemg21  40096  dibord  40569  lclkrlem2u  40937  lcfrlem9  40960  mapdindp4  41133  hdmaprnlem3uN  41261  hdmaprnlem9N  41267  fsuppind  41745  binomcxplemnotnn0  43716  dstregt0  44586  stoweidlem31  45342  stoweidlem59  45370  wallispilem4  45379  dirkertrigeqlem2  45410  fourierdlem43  45461  fourierdlem65  45482  catprs  47940