Theorem eqnetrrd 3027

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2959

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ne 2960

This theorem is used by:  eqnetrrid  3034  3netr3d  3035  cantnflem1c  9725  eqsqrt2d  15580  tanval2  16345  tanval3  16346  tanhlt1  16372  pcadd  17111  efgsres  20003  gsumval3  20172  ablfac  20355  ablsimpgfind  20377  isdrngrd  21074  isdrngrdOLD  21076  lspsneq  21451  lebnumlem3  25339  minveclem4a  25806  evthicc  25835  ioorf  25949  deg1ldgn  26466  fta1blem  26544  vieta1lem1  26688  vieta1lem2  26689  vieta1  26690  tanregt0  26924  isosctrlem2  27204  angpieqvd  27216  chordthmlem2  27218  dcubic2  27229  dquartlem1  27236  dquart  27238  asinlem  27253  atandmcj  27294  2efiatan  27303  tanatan  27304  dvatan  27320  dmgmn0  27410  dmgmdivn0  27412  lgamgulmlem2  27414  gamne0  27430  nosep1o  28095  noetasuplem4  28150  footexALT  29250  footexlem1  29251  footexlem2  29252  dfprlng3  29483  ttgcontlem1  29519  wlkn0  30258  nrt2irr  31131  fsuppcurry1  33412  fsuppcurry2  33413  bcm1n  33483  mxidlirred  34101  dfufd2  34186  ply1dg1rt  34215  esplymhp  34311  irngnminplynz  34455  minplym1p  34456  minplynzm1p  34457  algextdeglem4  34463  constrrtll  34474  constrrtlc1  34475  constrrtcclem  34477  constrfin  34489  constrelextdg2  34490  cos9thpiminplylem2  34526  zarclssn  34616  sibfof  35083  finxpreclem2  38581  poimirlem9  38815  heicant  38841  heiborlem6  39016  lkrlspeqN  40494  cdlemg18d  42004  cdlemg21  42009  dibord  42482  lclkrlem2u  42850  lcfrlem9  42873  mapdindp4  43046  hdmaprnlem3uN  43174  hdmaprnlem9N  43180  fsuppind  43884  binomcxplemnotnn0  45601  dstregt0  46571  stoweidlem31  47314  stoweidlem59  47342  wallispilem4  47351  dirkertrigeqlem2  47382  fourierdlem43  47433  fourierdlem65  47454  catprs  50456  oppfrcl3  50577  lmdran  51185  cmdlan  51186  tanhvaltan  51248  tanhvalnegitan  51253  tanhadd  51258