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 251 . 2 (𝜑 → (𝐴𝐵 → ¬ 𝐶𝐷))
43necon4ad 2959 1 (𝜑 → (𝐶𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1541  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 206  df-ne 2941
This theorem is referenced by:  disji  5131  mul02lem2  11393  mhpmulcl  21698  xblss2ps  23914  xblss2  23915  lgsne0  26845  h1datomi  30872  eigorthi  31128  disjif  31847  lineintmo  35198  poimirlem6  36580  poimirlem7  36581  2llnmat  38481  2lnat  38741  tendospcanN  39980  dihmeetlem13N  40276  dochkrshp  40343  remul02  41360  remul01  41362  sn-0tie0  41394
  Copyright terms: Public domain W3C validator