Theorem neeqtrrd 2999

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

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

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 2701

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

This theorem is referenced by:  3netr4d  3002  ttukeylem7  10409  modsumfzodifsn  13851  expnprm  16814  symgextf1lem  19299  isabvd  20697  flimclslem  23869  chordthmlem  26740  atandmtan  26828  dchrptlem3  27175  noetasuplem4  27646  opphllem6  28697  nrt2irr  30417  unidifsnne  32480  pmtrcnel  33031  pmtrcnel2  33032  cycpmrn  33085  qsdrnglem2  33433  fedgmul  33598  irngnzply1  33658  minplyelirng  33682  irredminply  33683  signstfveq0a  34544  subfacp1lem5  35161  ovoliunnfl  37646  voliunnfl  37648  volsupnfl  37649  cdleme40n  40451  cdleme40w  40453  cdlemg33c  40691  cdlemg33e  40693  trlcocnvat  40707  cdlemh2  40799  cdlemh  40800  cdlemj3  40806  cdlemk24-3  40886  cdlemkfid1N  40904  erng1r  40978  dvalveclem  41008  tendoinvcl  41087  tendolinv  41088  tendorinv  41089  dihatlat  41317  mapdpglem18  41672  mapdpglem22  41676  baerlem5amN  41699  baerlem5bmN  41700  baerlem5abmN  41701  mapdindp1  41703  mapdindp4  41706  hdmap14lem4a  41854  uvcn0  42519  prjspner1  42603  nlimsuc  43418  imo72b2lem2  44144  imo72b2  44149  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx13starlem2  48060  islindeps2  48472  fucofvalne  49314