Theorem neeqtrrd 3010

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

Syntax hints:   → wi 4   = wceq 1548   ≠ wne 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ne 2937

This theorem is referenced by:  3netr4d  3013  iunopeqop  5465  ttukeylem7  10432  modsumfzodifsn  13901  expnprm  16868  symgextf1lem  19390  isabvd  20788  flimclslem  23971  chordthmlem  26818  atandmtan  26906  dchrptlem3  27251  noetasuplem4  27722  opphllem6  28842  nrt2irr  30565  unidifsnne  32628  pmtrcnel  33174  pmtrcnel2  33175  cycpmrn  33228  qsdrnglem2  33583  fedgmul  33827  irngnzply1  33887  minplyelirng  33911  irredminply  33912  signstfveq0a  34772  subfacp1lem5  35427  ovoliunnfl  38044  voliunnfl  38046  volsupnfl  38047  cdleme40n  40975  cdleme40w  40977  cdlemg33c  41215  cdlemg33e  41217  trlcocnvat  41231  cdlemh2  41323  cdlemh  41324  cdlemj3  41330  cdlemk24-3  41410  cdlemkfid1N  41428  erng1r  41502  dvalveclem  41532  tendoinvcl  41611  tendolinv  41612  tendorinv  41613  dihatlat  41841  mapdpglem18  42196  mapdpglem22  42200  baerlem5amN  42223  baerlem5bmN  42224  baerlem5abmN  42225  mapdindp1  42227  mapdindp4  42230  hdmap14lem4a  42378  uvcn0  43043  prjspner1  43091  nlimsuc  43900  imo72b2lem2  44626  imo72b2  44631  gpg5nbgrvtx03starlem2  48574  gpg5nbgrvtx13starlem2  48577  islindeps2  48988  fucofvalne  49829