Theorem neeqtrrd 3038

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  3netr4d  3041  iunopeqop  5505  ttukeylem7  10499  modsumfzodifsn  13980  expnprm  16962  symgextf1lem  19490  isabvd  20893  flimclslem  24110  chordthmlem  26963  atandmtan  27051  dchrptlem3  27396  noetasuplem4  27866  opphllem6  28992  nrt2irr  30765  unidifsnne  32823  pmtrcnel  33350  pmtrcnel2  33351  cycpmrn  33404  qsdrnglem2  33723  fedgmul  33966  irngnzply1  34026  minplyelirng  34050  irredminply  34051  signstfveq0a  34908  subfacp1lem5  35575  ovoliunnfl  38201  voliunnfl  38203  volsupnfl  38204  cdleme40n  41132  cdleme40w  41134  cdlemg33c  41372  cdlemg33e  41374  trlcocnvat  41388  cdlemh2  41480  cdlemh  41481  cdlemj3  41487  cdlemk24-3  41567  cdlemkfid1N  41585  erng1r  41659  dvalveclem  41689  tendoinvcl  41768  tendolinv  41769  tendorinv  41770  dihatlat  41998  mapdpglem18  42353  mapdpglem22  42357  baerlem5amN  42380  baerlem5bmN  42381  baerlem5abmN  42382  mapdindp1  42384  mapdindp4  42387  hdmap14lem4a  42535  uvcn0  43202  prjspner1  43250  nlimsuc  44059  imo72b2lem2  44785  imo72b2  44790  gpg5nbgrvtx03starlem2  48723  gpg5nbgrvtx13starlem2  48726  islindeps2  49148  fucofvalne  49988