Theorem neeqtrrd 3017

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 3012	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  3netr4d  3020  ttukeylem7  10202  modsumfzodifsn  13592  expnprm  16531  symgextf1lem  18943  isabvd  19995  flimclslem  23043  chordthmlem  25887  atandmtan  25975  dchrptlem3  26319  opphllem6  27017  unidifsnne  30785  pmtrcnel  31260  pmtrcnel2  31261  cycpmrn  31312  fedgmul  31614  signstfveq0a  32455  subfacp1lem5  33046  noetasuplem4  33866  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  cdleme40n  38409  cdleme40w  38411  cdlemg33c  38649  cdlemg33e  38651  trlcocnvat  38665  cdlemh2  38757  cdlemh  38758  cdlemj3  38764  cdlemk24-3  38844  cdlemkfid1N  38862  erng1r  38936  dvalveclem  38966  tendoinvcl  39045  tendolinv  39046  tendorinv  39047  dihatlat  39275  mapdpglem18  39630  mapdpglem22  39634  baerlem5amN  39657  baerlem5bmN  39658  baerlem5abmN  39659  mapdindp1  39661  mapdindp4  39664  hdmap14lem4a  39812  uvcn0  40190  prjspner1  40384  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2  41672  islindeps2  45712