Theorem neeqtrrd 3029

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ne 2956

This theorem is used by:  3netr4d  3032  iunopeqop  5498  ttukeylem7  10520  modsumfzodifsn  14011  expnprm  16997  symgextf1lem  19550  isabvd  20981  flimclslem  24213  chordthmlem  27072  atandmtan  27160  dchrptlem3  27505  noetasuplem4  27975  opphllem6  29110  angmgmaddov1  29270  prlngmid2  29321  nrt2irr  30956  unidifsnne  33014  pmtrcnel  33532  pmtrcnel2  33533  cycpmrn  33586  qsdrnglem2  33901  fedgmul  34144  irngnzply1  34204  minplyelirng  34228  irredminply  34229  signstfveq0a  35087  subfacp1lem5  35766  mh-inf3f1  37163  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  cdleme40n  41344  cdleme40w  41346  cdlemg33c  41584  cdlemg33e  41586  trlcocnvat  41600  cdlemh2  41692  cdlemh  41693  cdlemj3  41699  cdlemk24-3  41779  cdlemkfid1N  41797  erng1r  41871  dvalveclem  41901  tendoinvcl  41980  tendolinv  41981  tendorinv  41982  dihatlat  42210  mapdpglem18  42565  mapdpglem22  42569  baerlem5amN  42592  baerlem5bmN  42593  baerlem5abmN  42594  mapdindp1  42596  mapdindp4  42599  hdmap14lem4a  42747  uvcn0  43427  prjspner1  43475  nlimsuc  44284  imo72b2lem2  45010  imo72b2  45015  gpg5nbgrvtx03starlem2  48988  gpg5nbgrvtx13starlem2  48991  islindeps2  49416  fucofvalne  50254