Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq2d Structured version   Visualization version   GIF version

Theorem neeq2d 3067
 Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Hypothesis
Ref Expression
neeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
neeq2d (𝜑 → (𝐶𝐴𝐶𝐵))

Proof of Theorem neeq2d
StepHypRef Expression
1 neeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21eqeq2d 2832 . 2 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
32necon3bid 3051 1 (𝜑 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 3007 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 1971  ax-7 2016  ax-9 2125  ax-ext 2793 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814  df-ne 3008 This theorem is referenced by:  neeq2  3070  neeqtrd  3076  prneprprc  4764  fndifnfp  6911  f12dfv  7004  f13dfv  7005  infpssrlem4  9705  sqrt2irr  15581  dsmmval  20854  dsmmbas2  20857  frlmbas  20875  dfconn2  22003  alexsublem  22628  uc1pval  24719  mon1pval  24721  dchrsum2  25831  isinag  26611  uhgrwkspthlem2  27522  usgr2wlkneq  27524  usgr2trlspth  27529  lfgrn1cycl  27570  uspgrn2crct  27573  2pthdlem1  27695  3pthdlem1  27928  numclwwlk2lem1  28140  eigorth  29600  eighmorth  29726  prmidlval  30964  mxidlval  30981  wlimeq12  33114  limsucncmpi  33801  poimirlem25  34964  poimirlem26  34965  pridlval  35353  maxidlval  35359  lshpset  36156  lduallkr3  36340  isatl  36477  cdlemk42  38119  dffltz  39422  stoweidlem43  42504  nnfoctbdjlem  42913
 Copyright terms: Public domain W3C validator