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

Theorem necon1d 3038
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 3020 . . 3 𝐶𝐷𝐶 = 𝐷)
31, 2syl6ibr 253 . 2 (𝜑 → (𝐴𝐵 → ¬ 𝐶𝐷))
43necon4ad 3035 1 (𝜑 → (𝐶𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  disji  5041  mul02lem2  10806  xblss2ps  22940  xblss2  22941  lgsne0  25839  h1datomi  29286  eigorthi  29542  disjif  30257  lineintmo  33516  poimirlem6  34780  poimirlem7  34781  2llnmat  36542  2lnat  36802  tendospcanN  38041  dihmeetlem13N  38337  dochkrshp  38404  remul02  39115  remul01  39117
  Copyright terms: Public domain W3C validator