Theorem neeqtrrd 2897

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

Syntax hints:   → wi 4   = wceq 1523   ≠ wne 2823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824

This theorem is referenced by:  3netr4d  2900  ttukeylem7  9375  modsumfzodifsn  12783  znnenlem  14984  expnprm  15653  symgextf1lem  17886  isabvd  18868  flimclslem  21835  chordthmlem  24604  atandmtan  24692  dchrptlem3  25036  opphllem6  25689  signstfveq0a  30781  subfacp1lem5  31292  noetalem3  31990  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  cdleme40n  36073  cdleme40w  36075  cdlemg33c  36313  cdlemg33e  36315  trlcocnvat  36329  cdlemh2  36421  cdlemh  36422  cdlemj3  36428  cdlemk24-3  36508  cdlemkfid1N  36526  erng1r  36600  dvalveclem  36631  tendoinvcl  36710  tendolinv  36711  tendorinv  36712  dihatlat  36940  mapdpglem18  37295  mapdpglem22  37299  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdindp1  37326  mapdindp4  37329  hdmap14lem4a  37480  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  islindeps2  42597