Theorem neeqtrrd 3033

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
neeqtrrd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
neeqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
neeqtrrd	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem neeqtrrd

Step	Hyp	Ref	Expression
1		neeqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		neeqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2769	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	neeqtrd 3028	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:  3netr4d  3036  iunopeqop  5501  ttukeylem7  10632  modsumfzodifsn  14127  expnprm  17124  symgextf1lem  19685  isabvd  21120  flimclslem  24358  chordthmlem  27217  atandmtan  27305  dchrptlem3  27650  flt4  28048  noetasuplem4  28150  opphllem6  29285  angmgmaddov1  29445  prlngmid2  29496  nrt2irr  31131  unidifsnne  33230  pmtrcnel  33749  pmtrcnel2  33750  cycpmrn  33803  qsdrnglem2  34124  fedgmul  34374  irngnzply1  34434  minplyelirng  34458  irredminply  34459  signstfveq0a  35316  ecscottd  35885  subfacp1lem5  36157  mh-inf3f1  37544  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  cdleme40n  41791  cdleme40w  41793  cdlemg33c  42031  cdlemg33e  42033  trlcocnvat  42047  cdlemh2  42139  cdlemh  42140  cdlemj3  42146  cdlemk24-3  42226  cdlemkfid1N  42244  erng1r  42318  dvalveclem  42348  tendoinvcl  42427  tendolinv  42428  tendorinv  42429  dihatlat  42657  mapdpglem18  43012  mapdpglem22  43016  baerlem5amN  43039  baerlem5bmN  43040  baerlem5abmN  43041  mapdindp1  43043  mapdindp4  43046  hdmap14lem4a  43194  uvcn0  43872  frlmnzcoordsca  43924  nlimsuc  44703  imo72b2lem2  45428  imo72b2  45433  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx13starlem2  49443  islindeps2  49926  fucofvalne  50778