Theorem eqnetrrd 3015

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  eqnetrrid  3022  3netr3d  3023  cantnflem1c  9756  eqsqrt2d  15417  tanval2  16181  tanval3  16182  tanhlt1  16208  pcadd  16936  efgsres  19780  gsumval3  19949  ablfac  20132  ablsimpgfind  20154  isdrngrd  20788  isdrngrdOLD  20790  lspsneq  21147  lebnumlem3  25014  minveclem4a  25483  evthicc  25513  ioorf  25627  deg1ldgn  26152  fta1blem  26230  vieta1lem1  26370  vieta1lem2  26371  vieta1  26372  tanregt0  26599  isosctrlem2  26880  angpieqvd  26892  chordthmlem2  26894  dcubic2  26905  dquartlem1  26912  dquart  26914  asinlem  26929  atandmcj  26970  2efiatan  26979  tanatan  26980  dvatan  26996  dmgmn0  27087  dmgmdivn0  27089  lgamgulmlem2  27091  gamne0  27107  nosep1o  27744  noetasuplem4  27799  footexALT  28744  footexlem1  28745  footexlem2  28746  ttgcontlem1  28917  wlkn0  29657  nrt2irr  30505  fsuppcurry1  32739  fsuppcurry2  32740  bcm1n  32800  mxidlirred  33465  dfufd2  33543  ply1dg1rt  33569  irngnminplynz  33705  minplym1p  33706  algextdeglem4  33711  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrfin  33736  constrelextdg2  33737  zarclssn  33819  sibfof  34305  finxpreclem2  37356  poimirlem9  37589  heicant  37615  heiborlem6  37776  lkrlspeqN  39127  cdlemg18d  40638  cdlemg21  40643  dibord  41116  lclkrlem2u  41484  lcfrlem9  41507  mapdindp4  41680  hdmaprnlem3uN  41808  hdmaprnlem9N  41814  fsuppind  42545  binomcxplemnotnn0  44325  dstregt0  45196  stoweidlem31  45952  stoweidlem59  45980  wallispilem4  45989  dirkertrigeqlem2  46020  fourierdlem43  46071  fourierdlem65  46092  catprs  48678