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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  3netr4d  3009  ttukeylem7  10529  modsumfzodifsn  13962  expnprm  16922  symgextf1lem  19401  isabvd  20772  flimclslem  23922  chordthmlem  26794  atandmtan  26882  dchrptlem3  27229  noetasuplem4  27700  opphllem6  28731  nrt2irr  30454  unidifsnne  32517  pmtrcnel  33100  pmtrcnel2  33101  cycpmrn  33154  qsdrnglem2  33511  fedgmul  33671  irngnzply1  33732  minplyelirng  33749  irredminply  33750  signstfveq0a  34608  subfacp1lem5  35206  ovoliunnfl  37686  voliunnfl  37688  volsupnfl  37689  cdleme40n  40487  cdleme40w  40489  cdlemg33c  40727  cdlemg33e  40729  trlcocnvat  40743  cdlemh2  40835  cdlemh  40836  cdlemj3  40842  cdlemk24-3  40922  cdlemkfid1N  40940  erng1r  41014  dvalveclem  41044  tendoinvcl  41123  tendolinv  41124  tendorinv  41125  dihatlat  41353  mapdpglem18  41708  mapdpglem22  41712  baerlem5amN  41735  baerlem5bmN  41736  baerlem5abmN  41737  mapdindp1  41739  mapdindp4  41742  hdmap14lem4a  41890  uvcn0  42565  prjspner1  42649  nlimsuc  43465  imo72b2lem2  44191  imo72b2  44196  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx13starlem2  48074  islindeps2  48459  fucofvalne  49236