Theorem neeqtrrd 3034

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  3netr4d  3037  iunopeqop  5506  ttukeylem7  10514  modsumfzodifsn  14000  expnprm  16986  symgextf1lem  19536  isabvd  20967  flimclslem  24194  chordthmlem  27050  atandmtan  27138  dchrptlem3  27483  noetasuplem4  27953  opphllem6  29086  prlngmid2  29268  nrt2irr  30897  unidifsnne  32955  pmtrcnel  33475  pmtrcnel2  33476  cycpmrn  33529  qsdrnglem2  33844  fedgmul  34087  irngnzply1  34147  minplyelirng  34171  irredminply  34172  signstfveq0a  35030  subfacp1lem5  35715  ovoliunnfl  38372  voliunnfl  38374  volsupnfl  38375  cdleme40n  41302  cdleme40w  41304  cdlemg33c  41542  cdlemg33e  41544  trlcocnvat  41558  cdlemh2  41650  cdlemh  41651  cdlemj3  41657  cdlemk24-3  41737  cdlemkfid1N  41755  erng1r  41829  dvalveclem  41859  tendoinvcl  41938  tendolinv  41939  tendorinv  41940  dihatlat  42168  mapdpglem18  42523  mapdpglem22  42527  baerlem5amN  42550  baerlem5bmN  42551  baerlem5abmN  42552  mapdindp1  42554  mapdindp4  42557  hdmap14lem4a  42705  uvcn0  43370  prjspner1  43418  nlimsuc  44227  imo72b2lem2  44953  imo72b2  44958  gpg5nbgrvtx03starlem2  48894  gpg5nbgrvtx13starlem2  48897  islindeps2  49322  fucofvalne  50162