Theorem neeqtrrd 3000

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  3netr4d  3003  ttukeylem7  10475  modsumfzodifsn  13916  expnprm  16880  symgextf1lem  19357  isabvd  20728  flimclslem  23878  chordthmlem  26749  atandmtan  26837  dchrptlem3  27184  noetasuplem4  27655  opphllem6  28686  nrt2irr  30409  unidifsnne  32472  pmtrcnel  33053  pmtrcnel2  33054  cycpmrn  33107  qsdrnglem2  33474  fedgmul  33634  irngnzply1  33693  minplyelirng  33712  irredminply  33713  signstfveq0a  34574  subfacp1lem5  35178  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  cdleme40n  40469  cdleme40w  40471  cdlemg33c  40709  cdlemg33e  40711  trlcocnvat  40725  cdlemh2  40817  cdlemh  40818  cdlemj3  40824  cdlemk24-3  40904  cdlemkfid1N  40922  erng1r  40996  dvalveclem  41026  tendoinvcl  41105  tendolinv  41106  tendorinv  41107  dihatlat  41335  mapdpglem18  41690  mapdpglem22  41694  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdindp1  41721  mapdindp4  41724  hdmap14lem4a  41872  uvcn0  42537  prjspner1  42621  nlimsuc  43437  imo72b2lem2  44163  imo72b2  44168  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067  islindeps2  48476  fucofvalne  49318