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

Theorem necon4d 2984
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon4d.1 (𝜑 → (𝐴𝐵𝐶𝐷))
Assertion
Ref Expression
necon4d (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))

Proof of Theorem necon4d
StepHypRef Expression
1 necon4d.1 . . 3 (𝜑 → (𝐴𝐵𝐶𝐷))
21necon2bd 2976 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2964 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3imbitrdi 254 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1563  wne 2960
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 210  df-ne 2961
This theorem is referenced by:  oa00  8532  map0g  8870  epfrs  9688  fin23lem24  10294  abs00  15330  oddvds  19608  01eq0ringOLD  20606  isdomn4  20791  isabvd  20884  uvcf1  21902  lindff1  21930  hausnei2  23471  dfconn2  23537  hausflimi  24098  hauspwpwf1  24105  cxpeq0  26801  his6  31360  fnpreimac  32927  deg1le0eq0  33780  lkreqN  39806  ltrnideq  40811  hdmapip0  42551  sticksstones2  42776  unitscyglem4  42827  rpnnen3  43621
  Copyright terms: Public domain W3C validator