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

Theorem necon1d 2993
Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon1d.1 (𝜑 → (𝐴𝐵𝐶 = 𝐷))
Assertion
Ref Expression
necon1d (𝜑 → (𝐶𝐷𝐴 = 𝐵))

Proof of Theorem necon1d
StepHypRef Expression
1 necon1d.1 . . 3 (𝜑 → (𝐴𝐵𝐶 = 𝐷))
2 nne 2975 . . 3 𝐶𝐷𝐶 = 𝐷)
31, 2syl6ibr 244 . 2 (𝜑 → (𝐴𝐵 → ¬ 𝐶𝐷))
43necon4ad 2990 1 (𝜑 → (𝐶𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1653  wne 2971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 199  df-ne 2972
This theorem is referenced by:  disji  4828  mul02lem2  10503  xblss2ps  22534  xblss2  22535  lgsne0  25412  h1datomi  28965  eigorthi  29221  disjif  29908  lineintmo  32777  poimirlem6  33904  poimirlem7  33905  2llnmat  35545  2lnat  35805  tendospcanN  37044  dihmeetlem13N  37340  dochkrshp  37407
  Copyright terms: Public domain W3C validator