Theorem neeqtrrd 3032

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ne 2959

This theorem is used by:  3netr4d  3035  iunopeqop  5497  ttukeylem7  10603  modsumfzodifsn  14097  expnprm  17092  symgextf1lem  19646  isabvd  21081  flimclslem  24315  chordthmlem  27172  atandmtan  27260  dchrptlem3  27605  flt4  28003  noetasuplem4  28105  opphllem6  29240  angmgmaddov1  29400  prlngmid2  29451  nrt2irr  31086  unidifsnne  33186  pmtrcnel  33703  pmtrcnel2  33704  cycpmrn  33757  qsdrnglem2  34073  fedgmul  34316  irngnzply1  34376  minplyelirng  34400  irredminply  34401  signstfveq0a  35258  ecscottd  35823  subfacp1lem5  36070  mh-inf3f1  37456  ovoliunnfl  38720  voliunnfl  38722  volsupnfl  38723  cdleme40n  41665  cdleme40w  41667  cdlemg33c  41905  cdlemg33e  41907  trlcocnvat  41921  cdlemh2  42013  cdlemh  42014  cdlemj3  42020  cdlemk24-3  42100  cdlemkfid1N  42118  erng1r  42192  dvalveclem  42222  tendoinvcl  42301  tendolinv  42302  tendorinv  42303  dihatlat  42531  mapdpglem18  42886  mapdpglem22  42890  baerlem5amN  42913  baerlem5bmN  42914  baerlem5abmN  42915  mapdindp1  42917  mapdindp4  42920  hdmap14lem4a  43068  uvcn0  43746  frlmnzcoordsca  43798  nlimsuc  44582  imo72b2lem2  45307  imo72b2  45312  gpg5nbgrvtx03starlem2  49306  gpg5nbgrvtx13starlem2  49309  islindeps2  49734  fucofvalne  50586