Theorem neeqtrrd 3012

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

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  3netr4d  3015  ttukeylem7  10552  modsumfzodifsn  13981  expnprm  16935  symgextf1lem  19452  isabvd  20829  flimclslem  24007  chordthmlem  26889  atandmtan  26977  dchrptlem3  27324  noetasuplem4  27795  opphllem6  28774  nrt2irr  30501  unidifsnne  32561  pmtrcnel  33091  pmtrcnel2  33092  cycpmrn  33145  qsdrnglem2  33503  fedgmul  33658  irngnzply1  33705  irredminply  33721  signstfveq0a  34569  subfacp1lem5  35168  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  cdleme40n  40450  cdleme40w  40452  cdlemg33c  40690  cdlemg33e  40692  trlcocnvat  40706  cdlemh2  40798  cdlemh  40799  cdlemj3  40805  cdlemk24-3  40885  cdlemkfid1N  40903  erng1r  40977  dvalveclem  41007  tendoinvcl  41086  tendolinv  41087  tendorinv  41088  dihatlat  41316  mapdpglem18  41671  mapdpglem22  41675  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdindp1  41702  mapdindp4  41705  hdmap14lem4a  41853  uvcn0  42528  prjspner1  42612  nlimsuc  43430  imo72b2lem2  44156  imo72b2  44161  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  islindeps2  48328