Theorem neeqtrrd 3006

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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  3netr4d  3009  iunopeqop  5475  ttukeylem7  10437  modsumfzodifsn  13906  expnprm  16873  symgextf1lem  19395  isabvd  20789  flimclslem  23949  chordthmlem  26796  atandmtan  26884  dchrptlem3  27229  noetasuplem4  27700  opphllem6  28820  nrt2irr  30543  unidifsnne  32606  pmtrcnel  33150  pmtrcnel2  33151  cycpmrn  33204  qsdrnglem2  33556  fedgmul  33775  irngnzply1  33835  minplyelirng  33859  irredminply  33860  signstfveq0a  34720  subfacp1lem5  35366  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  cdleme40n  40914  cdleme40w  40916  cdlemg33c  41154  cdlemg33e  41156  trlcocnvat  41170  cdlemh2  41262  cdlemh  41263  cdlemj3  41269  cdlemk24-3  41349  cdlemkfid1N  41367  erng1r  41441  dvalveclem  41471  tendoinvcl  41550  tendolinv  41551  tendorinv  41552  dihatlat  41780  mapdpglem18  42135  mapdpglem22  42139  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdindp1  42166  mapdindp4  42169  hdmap14lem4a  42317  uvcn0  42987  prjspner1  43059  nlimsuc  43868  imo72b2lem2  44594  imo72b2  44599  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  islindeps2  48959  fucofvalne  49800