Theorem neeqtrrd 3007

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  3netr4d  3010  ttukeylem7  10431  modsumfzodifsn  13900  expnprm  16867  symgextf1lem  19389  isabvd  20783  flimclslem  23962  chordthmlem  26812  atandmtan  26900  dchrptlem3  27246  noetasuplem4  27717  opphllem6  28837  nrt2irr  30561  unidifsnne  32624  pmtrcnel  33168  pmtrcnel2  33169  cycpmrn  33222  qsdrnglem2  33574  fedgmul  33794  irngnzply1  33854  minplyelirng  33878  irredminply  33879  signstfveq0a  34739  subfacp1lem5  35385  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  cdleme40n  40931  cdleme40w  40933  cdlemg33c  41171  cdlemg33e  41173  trlcocnvat  41187  cdlemh2  41279  cdlemh  41280  cdlemj3  41286  cdlemk24-3  41366  cdlemkfid1N  41384  erng1r  41458  dvalveclem  41488  tendoinvcl  41567  tendolinv  41568  tendorinv  41569  dihatlat  41797  mapdpglem18  42152  mapdpglem22  42156  baerlem5amN  42179  baerlem5bmN  42180  baerlem5abmN  42181  mapdindp1  42183  mapdindp4  42186  hdmap14lem4a  42334  uvcn0  43004  prjspner1  43076  nlimsuc  43889  imo72b2lem2  44615  imo72b2  44620  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  islindeps2  48974  fucofvalne  49815