Theorem neeqtrrd 3008

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

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  3netr4d  3011  iunopeqop  5462  ttukeylem7  10428  modsumfzodifsn  13897  expnprm  16864  symgextf1lem  19386  isabvd  20784  flimclslem  23967  chordthmlem  26814  atandmtan  26902  dchrptlem3  27247  noetasuplem4  27718  opphllem6  28838  nrt2irr  30561  unidifsnne  32624  pmtrcnel  33170  pmtrcnel2  33171  cycpmrn  33224  qsdrnglem2  33579  fedgmul  33815  irngnzply1  33875  minplyelirng  33899  irredminply  33900  signstfveq0a  34760  subfacp1lem5  35412  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  cdleme40n  40960  cdleme40w  40962  cdlemg33c  41200  cdlemg33e  41202  trlcocnvat  41216  cdlemh2  41308  cdlemh  41309  cdlemj3  41315  cdlemk24-3  41395  cdlemkfid1N  41413  erng1r  41487  dvalveclem  41517  tendoinvcl  41596  tendolinv  41597  tendorinv  41598  dihatlat  41826  mapdpglem18  42181  mapdpglem22  42185  baerlem5amN  42208  baerlem5bmN  42209  baerlem5abmN  42210  mapdindp1  42212  mapdindp4  42215  hdmap14lem4a  42363  uvcn0  43028  prjspner1  43076  nlimsuc  43885  imo72b2lem2  44611  imo72b2  44616  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  islindeps2  48974  fucofvalne  49815