Theorem neeqtrrd 3021

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  3netr4d  3024  ttukeylem7  10584  modsumfzodifsn  13995  expnprm  16949  symgextf1lem  19462  isabvd  20835  flimclslem  24013  chordthmlem  26893  atandmtan  26981  dchrptlem3  27328  noetasuplem4  27799  opphllem6  28778  nrt2irr  30505  unidifsnne  32564  pmtrcnel  33082  pmtrcnel2  33083  cycpmrn  33136  qsdrnglem2  33489  fedgmul  33644  irngnzply1  33691  irredminply  33707  signstfveq0a  34553  subfacp1lem5  35152  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  cdleme40n  40425  cdleme40w  40427  cdlemg33c  40665  cdlemg33e  40667  trlcocnvat  40681  cdlemh2  40773  cdlemh  40774  cdlemj3  40780  cdlemk24-3  40860  cdlemkfid1N  40878  erng1r  40952  dvalveclem  40982  tendoinvcl  41061  tendolinv  41062  tendorinv  41063  dihatlat  41291  mapdpglem18  41646  mapdpglem22  41650  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdindp1  41677  mapdindp4  41680  hdmap14lem4a  41828  uvcn0  42497  prjspner1  42581  nlimsuc  43403  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2  44134  islindeps2  48212