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  10444  modsumfzodifsn  13885  expnprm  16849  symgextf1lem  19334  isabvd  20732  flimclslem  23904  chordthmlem  26775  atandmtan  26863  dchrptlem3  27210  noetasuplem4  27681  opphllem6  28732  nrt2irr  30452  unidifsnne  32515  pmtrcnel  33061  pmtrcnel2  33062  cycpmrn  33115  qsdrnglem2  33460  fedgmul  33620  irngnzply1  33679  minplyelirng  33698  irredminply  33699  signstfveq0a  34560  subfacp1lem5  35164  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  cdleme40n  40455  cdleme40w  40457  cdlemg33c  40695  cdlemg33e  40697  trlcocnvat  40711  cdlemh2  40803  cdlemh  40804  cdlemj3  40810  cdlemk24-3  40890  cdlemkfid1N  40908  erng1r  40982  dvalveclem  41012  tendoinvcl  41091  tendolinv  41092  tendorinv  41093  dihatlat  41321  mapdpglem18  41676  mapdpglem22  41680  baerlem5amN  41703  baerlem5bmN  41704  baerlem5abmN  41705  mapdindp1  41707  mapdindp4  41710  hdmap14lem4a  41858  uvcn0  42523  prjspner1  42607  nlimsuc  43423  imo72b2lem2  44149  imo72b2  44154  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx13starlem2  48056  islindeps2  48465  fucofvalne  49307