Theorem neeqtrrd 2868

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

Syntax hints:   → wi 4   = wceq 1483   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  3netr4d  2871  ttukeylem7  9337  modsumfzodifsn  12743  znnenlem  14940  expnprm  15606  symgextf1lem  17840  isabvd  18820  flimclslem  21788  chordthmlem  24559  atandmtan  24647  dchrptlem3  24991  opphllem6  25644  signstfveq0a  30653  subfacp1lem5  31166  noetalem3  31865  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  cdleme40n  35756  cdleme40w  35758  cdlemg33c  35996  cdlemg33e  35998  trlcocnvat  36012  cdlemh2  36104  cdlemh  36105  cdlemj3  36111  cdlemk24-3  36191  cdlemkfid1N  36209  erng1r  36283  dvalveclem  36314  tendoinvcl  36393  tendolinv  36394  tendorinv  36395  dihatlat  36623  mapdpglem18  36978  mapdpglem22  36982  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdindp1  37009  mapdindp4  37012  hdmap14lem4a  37163  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  islindeps2  42272