Theorem neeqtrrd 3000

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

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

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 2120  ax-ext 2702

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

This theorem is referenced by:  3netr4d  3003  ttukeylem7  10398  modsumfzodifsn  13843  expnprm  16806  symgextf1lem  19325  isabvd  20720  flimclslem  23892  chordthmlem  26762  atandmtan  26850  dchrptlem3  27197  noetasuplem4  27668  opphllem6  28723  nrt2irr  30443  unidifsnne  32506  pmtrcnel  33048  pmtrcnel2  33049  cycpmrn  33102  qsdrnglem2  33451  fedgmul  33634  irngnzply1  33694  minplyelirng  33718  irredminply  33719  signstfveq0a  34579  subfacp1lem5  35196  ovoliunnfl  37681  voliunnfl  37683  volsupnfl  37684  cdleme40n  40486  cdleme40w  40488  cdlemg33c  40726  cdlemg33e  40728  trlcocnvat  40742  cdlemh2  40834  cdlemh  40835  cdlemj3  40841  cdlemk24-3  40921  cdlemkfid1N  40939  erng1r  41013  dvalveclem  41043  tendoinvcl  41122  tendolinv  41123  tendorinv  41124  dihatlat  41352  mapdpglem18  41707  mapdpglem22  41711  baerlem5amN  41734  baerlem5bmN  41735  baerlem5abmN  41736  mapdindp1  41738  mapdindp4  41741  hdmap14lem4a  41889  uvcn0  42554  prjspner1  42638  nlimsuc  43453  imo72b2lem2  44179  imo72b2  44184  gpg5nbgrvtx03starlem2  48079  gpg5nbgrvtx13starlem2  48082  islindeps2  48494  fucofvalne  49336