Theorem neeqtrrd 3004

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

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

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 2123  ax-ext 2706

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

This theorem is referenced by:  3netr4d  3007  ttukeylem7  10423  modsumfzodifsn  13865  expnprm  16828  symgextf1lem  19347  isabvd  20743  flimclslem  23926  chordthmlem  26796  atandmtan  26884  dchrptlem3  27231  noetasuplem4  27702  opphllem6  28773  nrt2irr  30497  unidifsnne  32560  pmtrcnel  33120  pmtrcnel2  33121  cycpmrn  33174  qsdrnglem2  33526  fedgmul  33737  irngnzply1  33797  minplyelirng  33821  irredminply  33822  signstfveq0a  34682  subfacp1lem5  35327  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  cdleme40n  40667  cdleme40w  40669  cdlemg33c  40907  cdlemg33e  40909  trlcocnvat  40923  cdlemh2  41015  cdlemh  41016  cdlemj3  41022  cdlemk24-3  41102  cdlemkfid1N  41120  erng1r  41194  dvalveclem  41224  tendoinvcl  41303  tendolinv  41304  tendorinv  41305  dihatlat  41533  mapdpglem18  41888  mapdpglem22  41892  baerlem5amN  41915  baerlem5bmN  41916  baerlem5abmN  41917  mapdindp1  41919  mapdindp4  41922  hdmap14lem4a  42070  uvcn0  42739  prjspner1  42811  nlimsuc  43624  imo72b2lem2  44350  imo72b2  44355  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  islindeps2  48671  fucofvalne  49512