Theorem neeqtrrd 3015

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 3010	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3netr4d  3018  ttukeylem7  10555  modsumfzodifsn  13985  expnprm  16940  symgextf1lem  19438  isabvd  20813  flimclslem  23992  chordthmlem  26875  atandmtan  26963  dchrptlem3  27310  noetasuplem4  27781  opphllem6  28760  nrt2irr  30492  unidifsnne  32554  pmtrcnel  33109  pmtrcnel2  33110  cycpmrn  33163  qsdrnglem2  33524  fedgmul  33682  irngnzply1  33741  irredminply  33757  signstfveq0a  34591  subfacp1lem5  35189  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  cdleme40n  40470  cdleme40w  40472  cdlemg33c  40710  cdlemg33e  40712  trlcocnvat  40726  cdlemh2  40818  cdlemh  40819  cdlemj3  40825  cdlemk24-3  40905  cdlemkfid1N  40923  erng1r  40997  dvalveclem  41027  tendoinvcl  41106  tendolinv  41107  tendorinv  41108  dihatlat  41336  mapdpglem18  41691  mapdpglem22  41695  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdindp1  41722  mapdindp4  41725  hdmap14lem4a  41873  uvcn0  42552  prjspner1  42636  nlimsuc  43454  imo72b2lem2  44180  imo72b2  44185  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  islindeps2  48400  fucofvalne  49020