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

Theorem necon1d 2960
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 2942 . . 3 𝐶𝐷𝐶 = 𝐷)
31, 2imbitrrdi 252 . 2 (𝜑 → (𝐴𝐵 → ¬ 𝐶𝐷))
43necon4ad 2957 1 (𝜑 → (𝐶𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1537  wne 2938
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 2939
This theorem is referenced by:  disji  5133  mul02lem2  11436  mhpmulcl  22171  xblss2ps  24427  xblss2  24428  lgsne0  27394  h1datomi  31610  eigorthi  31866  disjif  32598  lineintmo  36139  poimirlem6  37613  poimirlem7  37614  2llnmat  39507  2lnat  39767  tendospcanN  41006  dihmeetlem13N  41302  dochkrshp  41369  remul02  42412  remul01  42414  sn-0tie0  42446
  Copyright terms: Public domain W3C validator