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

Theorem necon2d 2998
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 2976 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2syl6ib 243 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 2990 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1653  wne 2975
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 199  df-ne 2976
This theorem is referenced by:  map0g  8140  cantnf  8844  hashprg  13436  bcthlem5  23458  deg1ldgn  24198  cxpeq0  24769  lfgrn1cycl  27060  uspgrn2crct  27063  poimirlem17  33919  poimirlem20  33922  poimirlem22  33924  poimirlem27  33929  islshpat  35042  cdleme18b  36317  cdlemh  36842
  Copyright terms: Public domain W3C validator