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

Theorem necon2d 2961
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 2939 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2imbitrdi 250 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
43necon2ad 2953 1 (𝜑 → (𝐶 = 𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2938
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 2939
This theorem is referenced by:  map0g  8880  cantnf  9690  hashprg  14359  bcthlem5  25076  deg1ldgn  25846  cxpeq0  26422  lfgrn1cycl  29326  uspgrn2crct  29329  poimirlem17  36808  poimirlem20  36811  poimirlem22  36813  poimirlem27  36818  islshpat  38190  cdleme18b  39466  cdlemh  39991  prjspner1  41670
  Copyright terms: Public domain W3C validator