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

Theorem necon2d 3039
Description: Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
Hypothesis
Ref Expression
necon2d.1 (𝜑 → (𝐴 = 𝐵𝐶𝐷))
Assertion
Ref Expression
necon2d (𝜑 → (𝐶 = 𝐷𝐴𝐵))

Proof of Theorem necon2d
StepHypRef Expression
1 necon2d.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶𝐷))
2 df-ne 3017 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2syl6ib 252 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 3031 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:  map0g  8438  cantnf  9145  hashprg  13746  bcthlem5  23860  deg1ldgn  24616  cxpeq0  25188  lfgrn1cycl  27511  uspgrn2crct  27514  poimirlem17  34791  poimirlem20  34794  poimirlem22  34796  poimirlem27  34801  islshpat  36035  cdleme18b  37310  cdlemh  37835
  Copyright terms: Public domain W3C validator