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

Theorem necon2d 2955
 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 2933 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2syl6ib 241 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 2947 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932 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 197  df-ne 2933 This theorem is referenced by:  map0g  8065  cantnf  8765  hashprg  13394  hashprgOLD  13395  bcthlem5  23345  deg1ldgn  24072  cxpeq0  24644  lfgrn1cycl  26929  uspgrn2crct  26932  poimirlem17  33757  poimirlem20  33760  poimirlem22  33762  poimirlem27  33767  islshpat  34825  cdleme18b  36100  cdlemh  36625
 Copyright terms: Public domain W3C validator