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  10512  modsumfzodifsn  13911  expnprm  16837  symgextf1lem  19290  isabvd  20432  flimclslem  23495  chordthmlem  26344  atandmtan  26432  dchrptlem3  26776  noetasuplem4  27246  opphllem6  28041  nrt2irr  29764  unidifsnne  31811  pmtrcnel  32291  pmtrcnel2  32292  cycpmrn  32343  qsdrnglem2  32655  fedgmul  32775  irngnzply1  32815  signstfveq0a  33656  subfacp1lem5  34244  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  cdleme40n  39425  cdleme40w  39427  cdlemg33c  39665  cdlemg33e  39667  trlcocnvat  39681  cdlemh2  39773  cdlemh  39774  cdlemj3  39780  cdlemk24-3  39860  cdlemkfid1N  39878  erng1r  39952  dvalveclem  39982  tendoinvcl  40061  tendolinv  40062  tendorinv  40063  dihatlat  40291  mapdpglem18  40646  mapdpglem22  40650  baerlem5amN  40673  baerlem5bmN  40674  baerlem5abmN  40675  mapdindp1  40677  mapdindp4  40680  hdmap14lem4a  40828  uvcn0  41194  prjspner1  41450  nlimsuc  42274  imo72b2lem0  42999  imo72b2lem2  43001  imo72b2  43006  islindeps2  47242