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

Theorem necon2d 2805
 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 2782 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2syl6ib 240 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 2797 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  map0g  7783  cantnf  8473  hashprg  13043  hashprgOLD  13044  bcthlem5  22933  deg1ldgn  23657  cxpeq0  24224  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem27  32606  islshpat  33322  cdleme18b  34597  cdlemh  35123  lfgrn1cycl  41008  uspgrn2crct  41011
 Copyright terms: Public domain W3C validator