Theorem neeqtrrd 3061

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

Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  3netr4d  3064  ttukeylem7  9926  modsumfzodifsn  13307  expnprm  16228  symgextf1lem  18540  isabvd  19584  flimclslem  22589  chordthmlem  25418  atandmtan  25506  dchrptlem3  25850  opphllem6  26546  unidifsnne  30308  pmtrcnel  30783  pmtrcnel2  30784  cycpmrn  30835  fedgmul  31115  signstfveq0a  31956  subfacp1lem5  32544  noetalem3  33332  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  cdleme40n  37764  cdleme40w  37766  cdlemg33c  38004  cdlemg33e  38006  trlcocnvat  38020  cdlemh2  38112  cdlemh  38113  cdlemj3  38119  cdlemk24-3  38199  cdlemkfid1N  38217  erng1r  38291  dvalveclem  38321  tendoinvcl  38400  tendolinv  38401  tendorinv  38402  dihatlat  38630  mapdpglem18  38985  mapdpglem22  38989  baerlem5amN  39012  baerlem5bmN  39013  baerlem5abmN  39014  mapdindp1  39016  mapdindp4  39019  hdmap14lem4a  39167  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2  40878  islindeps2  44892