Theorem neeqtrrd 3030

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  3netr4d  3033  iunopeqop  5494  ttukeylem7  10593  modsumfzodifsn  14087  expnprm  17080  symgextf1lem  19634  isabvd  21069  flimclslem  24303  chordthmlem  27160  atandmtan  27248  dchrptlem3  27593  flt4  27991  noetasuplem4  28093  opphllem6  29228  angmgmaddov1  29388  prlngmid2  29439  nrt2irr  31074  unidifsnne  33132  pmtrcnel  33650  pmtrcnel2  33651  cycpmrn  33704  qsdrnglem2  34020  fedgmul  34263  irngnzply1  34323  minplyelirng  34347  irredminply  34348  signstfveq0a  35205  subfacp1lem5  35949  mh-inf3f1  37329  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  cdleme40n  41525  cdleme40w  41527  cdlemg33c  41765  cdlemg33e  41767  trlcocnvat  41781  cdlemh2  41873  cdlemh  41874  cdlemj3  41880  cdlemk24-3  41960  cdlemkfid1N  41978  erng1r  42052  dvalveclem  42082  tendoinvcl  42161  tendolinv  42162  tendorinv  42163  dihatlat  42391  mapdpglem18  42746  mapdpglem22  42750  baerlem5amN  42773  baerlem5bmN  42774  baerlem5abmN  42775  mapdindp1  42777  mapdindp4  42780  hdmap14lem4a  42928  uvcn0  43606  frlmnzcoordsca  43658  nlimsuc  44441  imo72b2lem2  45166  imo72b2  45171  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  islindeps2  49594  fucofvalne  50432