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

Theorem necon2d 2964
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 2942 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2imbitrdi 250 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 2956 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2941
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 206  df-ne 2942
This theorem is referenced by:  map0g  8878  cantnf  9688  hashprg  14355  bcthlem5  24845  deg1ldgn  25611  cxpeq0  26186  lfgrn1cycl  29059  uspgrn2crct  29062  poimirlem17  36505  poimirlem20  36508  poimirlem22  36510  poimirlem27  36515  islshpat  37887  cdleme18b  39163  cdlemh  39688  prjspner1  41368
  Copyright terms: Public domain W3C validator