Theorem eqnetrrd 3009

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  eqnetrrid  3016  3netr3d  3017  cantnflem1c  9678  eqsqrt2d  15311  tanval2  16072  tanval3  16073  tanhlt1  16099  pcadd  16818  efgsres  19600  gsumval3  19769  ablfac  19952  ablsimpgfind  19974  isdrngrd  20341  isdrngrdOLD  20343  lspsneq  20727  lebnumlem3  24470  minveclem4a  24938  evthicc  24967  ioorf  25081  deg1ldgn  25602  fta1blem  25677  vieta1lem1  25814  vieta1lem2  25815  vieta1  25816  tanregt0  26039  isosctrlem2  26313  angpieqvd  26325  chordthmlem2  26327  dcubic2  26338  dquartlem1  26345  dquart  26347  asinlem  26362  atandmcj  26403  2efiatan  26412  tanatan  26413  dvatan  26429  dmgmn0  26519  dmgmdivn0  26521  lgamgulmlem2  26523  gamne0  26539  nosep1o  27173  noetasuplem4  27228  footexALT  27958  footexlem1  27959  footexlem2  27960  ttgcontlem1  28131  wlkn0  28867  fsuppcurry1  31937  fsuppcurry2  31938  bcm1n  31993  mxidlirred  32576  irngnminplynz  32759  algextdeglem1  32760  zarclssn  32841  sibfof  33327  finxpreclem2  36259  poimirlem9  36485  heicant  36511  heiborlem6  36672  lkrlspeqN  38029  cdlemg18d  39540  cdlemg21  39545  dibord  40018  lclkrlem2u  40386  lcfrlem9  40409  mapdindp4  40582  hdmaprnlem3uN  40710  hdmaprnlem9N  40716  fsuppind  41159  binomcxplemnotnn0  43100  dstregt0  43977  stoweidlem31  44733  stoweidlem59  44761  wallispilem4  44770  dirkertrigeqlem2  44801  fourierdlem43  44852  fourierdlem65  44873  catprs  47584