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

Theorem necon2d 3043
 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 3021 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2syl6ib 252 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 3035 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1530   ≠ wne 3020 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 3021 This theorem is referenced by:  map0g  8441  cantnf  9148  hashprg  13749  bcthlem5  23848  deg1ldgn  24604  cxpeq0  25176  lfgrn1cycl  27499  uspgrn2crct  27502  poimirlem17  34778  poimirlem20  34781  poimirlem22  34783  poimirlem27  34788  islshpat  36022  cdleme18b  37297  cdlemh  37822
 Copyright terms: Public domain W3C validator