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

Theorem necon2d 2962
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 2940 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2imbitrdi 251 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 2954 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2939
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 207  df-ne 2940
This theorem is referenced by:  map0g  8925  cantnf  9734  hashprg  14435  bcthlem5  25363  deg1ldgn  26133  cxpeq0  26721  lfgrn1cycl  29826  uspgrn2crct  29829  poimirlem17  37645  poimirlem20  37648  poimirlem22  37650  poimirlem27  37655  islshpat  39019  cdleme18b  40295  cdlemh  40820  prjspner1  42641
  Copyright terms: Public domain W3C validator