Theorem neeqtrd 3027

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

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

This theorem is used by:  neeqtrrd  3032  3netr3d  3034  xaddass2  13280  xov1plusxeqvd  13529  smndex2dnrinv  18981  ablsimpgfindlem1  20183  issubdrg  20892  0ringprmidl  21486  qsssubdrg  21585  ply1scln0  22461  alexsublem  24210  cphsubrglem  25345  cphreccllem  25346  mdegldg  26232  nosep2o  27855  noetainflem4  27913  tglinethru  28918  footexALT  29007  footexlem2  29009  lnssplng  29083  nrt2irr  30833  sdrgdvcl  33629  sdrginvcl  33630  0ringmon1p  33856  irngnzply1lem  34089  irngnminplynz  34111  minplym1p  34112  minplynzm1p  34113  algextdeglem4  34119  mh-inf3f1  37080  poimirlem26  38325  lkrpssN  39965  lnatexN  40581  lhpexle2lem  40811  lhpexle3lem  40813  cdlemg47  41538  cdlemk54  41760  tendoinvcl  41906  lcdlkreqN  42424  mapdh8ab  42579  aks6d1c5lem2  42933  aks6d1c7  42979  jm2.26lem3  43756  stoweidlem36  46778  addmodne  48115  p1modne  48118  m1modne  48119  minusmod5ne  48120  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx13starlem2  48865  gpg5edgnedg  48923