Theorem neeqtrrd 2855

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

Syntax hints:   → wi 4   = wceq 1474   ≠ wne 2779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781

This theorem is referenced by:  3netr4d  2858  ttukeylem7  9197  modsumfzodifsn  12560  znnenlem  14725  expnprm  15390  symgextf1lem  17609  isabvd  18589  flimclslem  21540  chordthmlem  24276  atandmtan  24364  dchrptlem3  24708  opphllem6  25362  isusgra0  25642  usgraop  25645  signstfveq0a  29785  subfacp1lem5  30226  nodenselem3  30888  ovoliunnfl  32417  voliunnfl  32419  volsupnfl  32420  cdleme40n  34570  cdleme40w  34572  cdlemg33c  34810  cdlemg33e  34812  trlcocnvat  34826  cdlemh2  34918  cdlemh  34919  cdlemj3  34925  cdlemk24-3  35005  cdlemkfid1N  35023  erng1r  35097  dvalveclem  35128  tendoinvcl  35207  tendolinv  35208  tendorinv  35209  dihatlat  35437  mapdpglem18  35792  mapdpglem22  35796  baerlem5amN  35819  baerlem5bmN  35820  baerlem5abmN  35821  mapdindp1  35823  mapdindp4  35826  hdmap14lem4a  35977  imo72b2lem0  37283  imo72b2lem2  37285  imo72b2lem1  37289  imo72b2  37293  islindeps2  42061