Theorem neeqtrd 3002

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
neeqtrd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
neeqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
neeqtrd	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem neeqtrd

Step	Hyp	Ref	Expression
1		neeqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		neeqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	neeq2d 2993	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  neeqtrrd  3007  3netr3d  3009  xaddass2  13197  xov1plusxeqvd  13446  smndex2dnrinv  18881  ablsimpgfindlem1  20079  issubdrg  20752  qsssubdrg  21420  ply1scln0  22270  alexsublem  24023  cphsubrglem  25158  cphreccllem  25159  mdegldg  26045  nosep2o  27664  noetainflem4  27722  tglinethru  28722  footexALT  28804  footexlem2  28806  nrt2irr  30562  sdrgdvcl  33379  sdrginvcl  33380  0ringprmidl  33528  0ringmon1p  33636  irngnzply1lem  33854  irngnminplynz  33876  minplym1p  33877  minplynzm1p  33878  algextdeglem4  33884  mh-inf3f1  36743  poimirlem26  37985  lkrpssN  39627  lnatexN  40243  lhpexle2lem  40473  lhpexle3lem  40475  cdlemg47  41200  cdlemk54  41422  tendoinvcl  41568  lcdlkreqN  42086  mapdh8ab  42241  aks6d1c5lem2  42595  aks6d1c7  42641  jm2.26lem3  43451  stoweidlem36  46486  addmodne  47814  p1modne  47817  m1modne  47818  minusmod5ne  47819  gpg5nbgrvtx03starlem2  48561  gpg5nbgrvtx13starlem2  48564  gpg5edgnedg  48622