Theorem neeqtrrd 3002

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  3netr4d  3005  ttukeylem7  10406  modsumfzodifsn  13851  expnprm  16814  symgextf1lem  19332  isabvd  20727  flimclslem  23899  chordthmlem  26769  atandmtan  26857  dchrptlem3  27204  noetasuplem4  27675  opphllem6  28730  nrt2irr  30453  unidifsnne  32516  pmtrcnel  33058  pmtrcnel2  33059  cycpmrn  33112  qsdrnglem2  33461  fedgmul  33644  irngnzply1  33704  minplyelirng  33728  irredminply  33729  signstfveq0a  34589  subfacp1lem5  35228  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  cdleme40n  40577  cdleme40w  40579  cdlemg33c  40817  cdlemg33e  40819  trlcocnvat  40833  cdlemh2  40925  cdlemh  40926  cdlemj3  40932  cdlemk24-3  41012  cdlemkfid1N  41030  erng1r  41104  dvalveclem  41134  tendoinvcl  41213  tendolinv  41214  tendorinv  41215  dihatlat  41443  mapdpglem18  41798  mapdpglem22  41802  baerlem5amN  41825  baerlem5bmN  41826  baerlem5abmN  41827  mapdindp1  41829  mapdindp4  41832  hdmap14lem4a  41980  uvcn0  42645  prjspner1  42729  nlimsuc  43544  imo72b2lem2  44270  imo72b2  44275  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx13starlem2  48182  islindeps2  48594  fucofvalne  49436