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

Theorem necon1d 2962
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 2944 . . 3 𝐶𝐷𝐶 = 𝐷)
31, 2imbitrrdi 252 . 2 (𝜑 → (𝐴𝐵 → ¬ 𝐶𝐷))
43necon4ad 2959 1 (𝜑 → (𝐶𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  disji  5128  mul02lem2  11438  mhpmulcl  22153  xblss2ps  24411  xblss2  24412  lgsne0  27379  h1datomi  31600  eigorthi  31856  disjif  32591  lineintmo  36158  poimirlem6  37633  poimirlem7  37634  2llnmat  39526  2lnat  39786  tendospcanN  41025  dihmeetlem13N  41321  dochkrshp  41388  remul02  42435  remul01  42437  sn-0tie0  42469  oppcthinendcALT  49090
  Copyright terms: Public domain W3C validator