Theorem neeqtrrd 2856

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

Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  3netr4d  2859  ttukeylem7  9220  modsumfzodifsn  12605  znnenlem  14779  expnprm  15444  symgextf1lem  17663  isabvd  18643  flimclslem  21598  chordthmlem  24359  atandmtan  24447  dchrptlem3  24791  opphllem6  25444  isusgra0  25876  usgraop  25879  signstfveq0a  29979  subfacp1lem5  30420  nodenselem3  31082  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  cdleme40n  34774  cdleme40w  34776  cdlemg33c  35014  cdlemg33e  35016  trlcocnvat  35030  cdlemh2  35122  cdlemh  35123  cdlemj3  35129  cdlemk24-3  35209  cdlemkfid1N  35227  erng1r  35301  dvalveclem  35332  tendoinvcl  35411  tendolinv  35412  tendorinv  35413  dihatlat  35641  mapdpglem18  35996  mapdpglem22  36000  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdindp1  36027  mapdindp4  36030  hdmap14lem4a  36181  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  islindeps2  42066