Theorem neeqtrd 3033

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 3024	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶))
4	1, 3	mpbid 235	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  neeqtrrd  3038  3netr3d  3040  xaddass2  13276  xov1plusxeqvd  13525  smndex2dnrinv  18977  ablsimpgfindlem1  20179  issubdrg  20861  0ringprmidl  21446  qsssubdrg  21545  ply1scln0  22421  alexsublem  24170  cphsubrglem  25305  cphreccllem  25306  mdegldg  26192  nosep2o  27812  noetainflem4  27870  tglinethru  28871  footexALT  28957  footexlem2  28959  lnssplng  29032  nrt2irr  30765  sdrgdvcl  33563  sdrginvcl  33564  0ringmon1p  33792  irngnzply1lem  34025  irngnminplynz  34047  minplym1p  34048  minplynzm1p  34049  algextdeglem4  34055  mh-inf3f1  36975  poimirlem26  38219  lkrpssN  39861  lnatexN  40477  lhpexle2lem  40707  lhpexle3lem  40709  cdlemg47  41434  cdlemk54  41656  tendoinvcl  41802  lcdlkreqN  42320  mapdh8ab  42475  aks6d1c5lem2  42829  aks6d1c7  42875  jm2.26lem3  43654  stoweidlem36  46676  addmodne  48010  p1modne  48013  m1modne  48014  minusmod5ne  48015  gpg5nbgrvtx03starlem2  48757  gpg5nbgrvtx13starlem2  48760  gpg5edgnedg  48818