Theorem neeqtrrd 3032

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  3netr4d  3035  iunopeqop  5504  ttukeylem7  10494  modsumfzodifsn  13976  expnprm  16957  symgextf1lem  19485  isabvd  20915  flimclslem  24141  chordthmlem  26997  atandmtan  27085  dchrptlem3  27430  noetasuplem4  27900  opphllem6  29033  prlngmid2  29211  nrt2irr  30824  unidifsnne  32882  pmtrcnel  33409  pmtrcnel2  33410  cycpmrn  33463  qsdrnglem2  33778  fedgmul  34021  irngnzply1  34081  minplyelirng  34105  irredminply  34106  signstfveq0a  34963  subfacp1lem5  35676  ovoliunnfl  38333  voliunnfl  38335  volsupnfl  38336  cdleme40n  41262  cdleme40w  41264  cdlemg33c  41502  cdlemg33e  41504  trlcocnvat  41518  cdlemh2  41610  cdlemh  41611  cdlemj3  41617  cdlemk24-3  41697  cdlemkfid1N  41715  erng1r  41789  dvalveclem  41819  tendoinvcl  41898  tendolinv  41899  tendorinv  41900  dihatlat  42128  mapdpglem18  42483  mapdpglem22  42487  baerlem5amN  42510  baerlem5bmN  42511  baerlem5abmN  42512  mapdindp1  42514  mapdindp4  42517  hdmap14lem4a  42665  uvcn0  43330  prjspner1  43378  nlimsuc  44187  imo72b2lem2  44913  imo72b2  44918  gpg5nbgrvtx03starlem2  48854  gpg5nbgrvtx13starlem2  48857  islindeps2  49283  fucofvalne  50123