Theorem neeqtrrd 3020

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2946

This theorem is referenced by:  3netr4d  3023  ttukeylem7  10272  modsumfzodifsn  13662  expnprm  16601  symgextf1lem  19026  isabvd  20078  flimclslem  23133  chordthmlem  25980  atandmtan  26068  dchrptlem3  26412  opphllem6  27111  unidifsnne  30880  pmtrcnel  31354  pmtrcnel2  31355  cycpmrn  31406  fedgmul  31708  signstfveq0a  32551  subfacp1lem5  33142  noetasuplem4  33935  ovoliunnfl  35815  voliunnfl  35817  volsupnfl  35818  cdleme40n  38478  cdleme40w  38480  cdlemg33c  38718  cdlemg33e  38720  trlcocnvat  38734  cdlemh2  38826  cdlemh  38827  cdlemj3  38833  cdlemk24-3  38913  cdlemkfid1N  38931  erng1r  39005  dvalveclem  39035  tendoinvcl  39114  tendolinv  39115  tendorinv  39116  dihatlat  39344  mapdpglem18  39699  mapdpglem22  39703  baerlem5amN  39726  baerlem5bmN  39727  baerlem5abmN  39728  mapdindp1  39730  mapdindp4  39733  hdmap14lem4a  39881  uvcn0  40262  prjspner1  40460  imo72b2lem0  41746  imo72b2lem2  41748  imo72b2  41753  islindeps2  45793