Theorem neeqtrrd 2999

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  3netr4d  3002  ttukeylem7  10468  modsumfzodifsn  13909  expnprm  16873  symgextf1lem  19350  isabvd  20721  flimclslem  23871  chordthmlem  26742  atandmtan  26830  dchrptlem3  27177  noetasuplem4  27648  opphllem6  28679  nrt2irr  30402  unidifsnne  32465  pmtrcnel  33046  pmtrcnel2  33047  cycpmrn  33100  qsdrnglem2  33467  fedgmul  33627  irngnzply1  33686  minplyelirng  33705  irredminply  33706  signstfveq0a  34567  subfacp1lem5  35171  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  cdleme40n  40462  cdleme40w  40464  cdlemg33c  40702  cdlemg33e  40704  trlcocnvat  40718  cdlemh2  40810  cdlemh  40811  cdlemj3  40817  cdlemk24-3  40897  cdlemkfid1N  40915  erng1r  40989  dvalveclem  41019  tendoinvcl  41098  tendolinv  41099  tendorinv  41100  dihatlat  41328  mapdpglem18  41683  mapdpglem22  41687  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdindp1  41714  mapdindp4  41717  hdmap14lem4a  41865  uvcn0  42530  prjspner1  42614  nlimsuc  43430  imo72b2lem2  44156  imo72b2  44161  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  islindeps2  48472  fucofvalne  49314