Theorem neeqtrrd 3006

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  3netr4d  3009  ttukeylem7  10425  modsumfzodifsn  13867  expnprm  16830  symgextf1lem  19349  isabvd  20745  flimclslem  23928  chordthmlem  26798  atandmtan  26886  dchrptlem3  27233  noetasuplem4  27704  opphllem6  28824  nrt2irr  30548  unidifsnne  32611  pmtrcnel  33171  pmtrcnel2  33172  cycpmrn  33225  qsdrnglem2  33577  fedgmul  33788  irngnzply1  33848  minplyelirng  33872  irredminply  33873  signstfveq0a  34733  subfacp1lem5  35378  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  cdleme40n  40738  cdleme40w  40740  cdlemg33c  40978  cdlemg33e  40980  trlcocnvat  40994  cdlemh2  41086  cdlemh  41087  cdlemj3  41093  cdlemk24-3  41173  cdlemkfid1N  41191  erng1r  41265  dvalveclem  41295  tendoinvcl  41374  tendolinv  41375  tendorinv  41376  dihatlat  41604  mapdpglem18  41959  mapdpglem22  41963  baerlem5amN  41986  baerlem5bmN  41987  baerlem5abmN  41988  mapdindp1  41990  mapdindp4  41993  hdmap14lem4a  42141  uvcn0  42807  prjspner1  42879  nlimsuc  43692  imo72b2lem2  44418  imo72b2  44423  gpg5nbgrvtx03starlem2  48325  gpg5nbgrvtx13starlem2  48328  islindeps2  48739  fucofvalne  49580