Theorem neeqtrrd 3004

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

Syntax hints:   → wi 4   = wceq 1533   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ne 2930

This theorem is referenced by:  3netr4d  3007  ttukeylem7  10540  modsumfzodifsn  13945  expnprm  16874  symgextf1lem  19387  isabvd  20712  flimclslem  23932  chordthmlem  26809  atandmtan  26897  dchrptlem3  27244  noetasuplem4  27715  opphllem6  28628  nrt2irr  30355  unidifsnne  32411  pmtrcnel  32902  pmtrcnel2  32903  cycpmrn  32956  qsdrnglem2  33308  fedgmul  33460  irngnzply1  33500  irredminply  33515  signstfveq0a  34339  subfacp1lem5  34925  ovoliunnfl  37266  voliunnfl  37268  volsupnfl  37269  cdleme40n  40071  cdleme40w  40073  cdlemg33c  40311  cdlemg33e  40313  trlcocnvat  40327  cdlemh2  40419  cdlemh  40420  cdlemj3  40426  cdlemk24-3  40506  cdlemkfid1N  40524  erng1r  40598  dvalveclem  40628  tendoinvcl  40707  tendolinv  40708  tendorinv  40709  dihatlat  40937  mapdpglem18  41292  mapdpglem22  41296  baerlem5amN  41319  baerlem5bmN  41320  baerlem5abmN  41321  mapdindp1  41323  mapdindp4  41326  hdmap14lem4a  41474  uvcn0  41910  prjspner1  42185  nlimsuc  43013  imo72b2lem0  43737  imo72b2lem2  43739  imo72b2  43744  islindeps2  47737