MPE Home 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