Theorem neeqtrrd 3007

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 2743	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	neeqtrd 3002	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  3netr4d  3010  ttukeylem7  10437  modsumfzodifsn  13879  expnprm  16842  symgextf1lem  19361  isabvd  20757  flimclslem  23940  chordthmlem  26810  atandmtan  26898  dchrptlem3  27245  noetasuplem4  27716  opphllem6  28836  nrt2irr  30560  unidifsnne  32623  pmtrcnel  33183  pmtrcnel2  33184  cycpmrn  33237  qsdrnglem2  33589  fedgmul  33809  irngnzply1  33869  minplyelirng  33893  irredminply  33894  signstfveq0a  34754  subfacp1lem5  35400  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  cdleme40n  40844  cdleme40w  40846  cdlemg33c  41084  cdlemg33e  41086  trlcocnvat  41100  cdlemh2  41192  cdlemh  41193  cdlemj3  41199  cdlemk24-3  41279  cdlemkfid1N  41297  erng1r  41371  dvalveclem  41401  tendoinvcl  41480  tendolinv  41481  tendorinv  41482  dihatlat  41710  mapdpglem18  42065  mapdpglem22  42069  baerlem5amN  42092  baerlem5bmN  42093  baerlem5abmN  42094  mapdindp1  42096  mapdindp4  42099  hdmap14lem4a  42247  uvcn0  42912  prjspner1  42984  nlimsuc  43797  imo72b2lem2  44523  imo72b2  44528  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx13starlem2  48432  islindeps2  48843  fucofvalne  49684