Theorem eqnetrrd 2993

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetrrid  3000  3netr3d  3001  cantnflem1c  9616  eqsqrt2d  15311  tanval2  16077  tanval3  16078  tanhlt1  16104  pcadd  16836  efgsres  19644  gsumval3  19813  ablfac  19996  ablsimpgfind  20018  isdrngrd  20651  isdrngrdOLD  20653  lspsneq  21008  lebnumlem3  24838  minveclem4a  25306  evthicc  25336  ioorf  25450  deg1ldgn  25974  fta1blem  26052  vieta1lem1  26194  vieta1lem2  26195  vieta1  26196  tanregt0  26424  isosctrlem2  26705  angpieqvd  26717  chordthmlem2  26719  dcubic2  26730  dquartlem1  26737  dquart  26739  asinlem  26754  atandmcj  26795  2efiatan  26804  tanatan  26805  dvatan  26821  dmgmn0  26912  dmgmdivn0  26914  lgamgulmlem2  26916  gamne0  26932  nosep1o  27569  noetasuplem4  27624  footexALT  28621  footexlem1  28622  footexlem2  28623  ttgcontlem1  28788  wlkn0  29524  nrt2irr  30375  fsuppcurry1  32621  fsuppcurry2  32622  bcm1n  32691  mxidlirred  33416  dfufd2  33494  ply1dg1rt  33521  irngnminplynz  33675  minplym1p  33676  minplynzm1p  33677  algextdeglem4  33683  constrrtll  33694  constrrtlc1  33695  constrrtcclem  33697  constrfin  33709  constrelextdg2  33710  cos9thpiminplylem2  33746  zarclssn  33836  sibfof  34304  finxpreclem2  37351  poimirlem9  37596  heicant  37622  heiborlem6  37783  lkrlspeqN  39137  cdlemg18d  40648  cdlemg21  40653  dibord  41126  lclkrlem2u  41494  lcfrlem9  41517  mapdindp4  41690  hdmaprnlem3uN  41818  hdmaprnlem9N  41824  fsuppind  42551  binomcxplemnotnn0  44318  dstregt0  45253  stoweidlem31  46002  stoweidlem59  46030  wallispilem4  46039  dirkertrigeqlem2  46070  fourierdlem43  46121  fourierdlem65  46142  catprs  48973  oppfrcl3  49092  lmdran  49633  cmdlan  49634