Theorem neeqtrrd 3031

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

Syntax hints:   → wi 4   = wceq 1560   ≠ wne 2957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ne 2958

This theorem is referenced by:  3netr4d  3034  iunopeqop  5490  ttukeylem7  10472  modsumfzodifsn  13957  expnprm  16938  symgextf1lem  19460  isabvd  20861  flimclslem  24044  chordthmlem  26897  atandmtan  26985  dchrptlem3  27330  noetasuplem4  27800  opphllem6  28925  nrt2irr  30675  unidifsnne  32735  pmtrcnel  33269  pmtrcnel2  33270  cycpmrn  33323  qsdrnglem2  33684  fedgmul  33928  irngnzply1  33988  minplyelirng  34012  irredminply  34013  signstfveq0a  34870  subfacp1lem5  35534  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  cdleme40n  41092  cdleme40w  41094  cdlemg33c  41332  cdlemg33e  41334  trlcocnvat  41348  cdlemh2  41440  cdlemh  41441  cdlemj3  41447  cdlemk24-3  41527  cdlemkfid1N  41545  erng1r  41619  dvalveclem  41649  tendoinvcl  41728  tendolinv  41729  tendorinv  41730  dihatlat  41958  mapdpglem18  42313  mapdpglem22  42317  baerlem5amN  42340  baerlem5bmN  42341  baerlem5abmN  42342  mapdindp1  42344  mapdindp4  42347  hdmap14lem4a  42495  uvcn0  43160  prjspner1  43208  nlimsuc  44017  imo72b2lem2  44743  imo72b2  44748  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx13starlem2  48694  islindeps2  49105  fucofvalne  49946