Theorem neeqtrrd 3018

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  3netr4d  3021  ttukeylem7  10271  modsumfzodifsn  13664  expnprm  16603  symgextf1lem  19028  isabvd  20080  flimclslem  23135  chordthmlem  25982  atandmtan  26070  dchrptlem3  26414  opphllem6  27113  unidifsnne  30884  pmtrcnel  31358  pmtrcnel2  31359  cycpmrn  31410  fedgmul  31712  signstfveq0a  32555  subfacp1lem5  33146  noetasuplem4  33939  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  cdleme40n  38482  cdleme40w  38484  cdlemg33c  38722  cdlemg33e  38724  trlcocnvat  38738  cdlemh2  38830  cdlemh  38831  cdlemj3  38837  cdlemk24-3  38917  cdlemkfid1N  38935  erng1r  39009  dvalveclem  39039  tendoinvcl  39118  tendolinv  39119  tendorinv  39120  dihatlat  39348  mapdpglem18  39703  mapdpglem22  39707  baerlem5amN  39730  baerlem5bmN  39731  baerlem5abmN  39732  mapdindp1  39734  mapdindp4  39737  hdmap14lem4a  39885  uvcn0  40265  prjspner1  40463  nlimsuc  41048  imo72b2lem0  41776  imo72b2lem2  41778  imo72b2  41783  islindeps2  45824