Theorem neeqtrrd 3016

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  3netr4d  3019  ttukeylem7  10510  modsumfzodifsn  13909  expnprm  16835  symgextf1lem  19288  isabvd  20428  flimclslem  23488  chordthmlem  26337  atandmtan  26425  dchrptlem3  26769  noetasuplem4  27239  opphllem6  28003  nrt2irr  29726  unidifsnne  31773  pmtrcnel  32250  pmtrcnel2  32251  cycpmrn  32302  qsdrnglem2  32610  fedgmul  32716  irngnzply1  32755  signstfveq0a  33587  subfacp1lem5  34175  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  cdleme40n  39339  cdleme40w  39341  cdlemg33c  39579  cdlemg33e  39581  trlcocnvat  39595  cdlemh2  39687  cdlemh  39688  cdlemj3  39694  cdlemk24-3  39774  cdlemkfid1N  39792  erng1r  39866  dvalveclem  39896  tendoinvcl  39975  tendolinv  39976  tendorinv  39977  dihatlat  40205  mapdpglem18  40560  mapdpglem22  40564  baerlem5amN  40587  baerlem5bmN  40588  baerlem5abmN  40589  mapdindp1  40591  mapdindp4  40594  hdmap14lem4a  40742  uvcn0  41112  prjspner1  41368  nlimsuc  42192  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2  42924  islindeps2  47164