Theorem neeqtrrd 3015

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  3netr4d  3018  ttukeylem7  10506  modsumfzodifsn  13905  expnprm  16831  symgextf1lem  19282  isabvd  20420  flimclslem  23479  chordthmlem  26326  atandmtan  26414  dchrptlem3  26758  noetasuplem4  27228  opphllem6  27992  unidifsnne  31760  pmtrcnel  32237  pmtrcnel2  32238  cycpmrn  32289  qsdrnglem2  32598  fedgmul  32704  irngnzply1  32743  signstfveq0a  33575  subfacp1lem5  34163  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  cdleme40n  39327  cdleme40w  39329  cdlemg33c  39567  cdlemg33e  39569  trlcocnvat  39583  cdlemh2  39675  cdlemh  39676  cdlemj3  39682  cdlemk24-3  39762  cdlemkfid1N  39780  erng1r  39854  dvalveclem  39884  tendoinvcl  39963  tendolinv  39964  tendorinv  39965  dihatlat  40193  mapdpglem18  40548  mapdpglem22  40552  baerlem5amN  40575  baerlem5bmN  40576  baerlem5abmN  40577  mapdindp1  40579  mapdindp4  40582  hdmap14lem4a  40730  uvcn0  41109  prjspner1  41364  nlimsuc  42177  imo72b2lem0  42902  imo72b2lem2  42904  imo72b2  42909  islindeps2  47117