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

Theorem necon4d 2964
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 2956 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2944 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3imbitrdi 251 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 2941
This theorem is referenced by:  oa00  8597  map0g  8924  epfrs  9771  fin23lem24  10362  abs00  15328  oddvds  19565  01eq0ringOLD  20531  isdomn4  20716  isabvd  20813  uvcf1  21812  lindff1  21840  hausnei2  23361  dfconn2  23427  hausflimi  23988  hauspwpwf1  23995  cxpeq0  26720  his6  31118  fnpreimac  32681  deg1le0eq0  33598  lkreqN  39171  ltrnideq  40177  hdmapip0  41917  sticksstones2  42148  unitscyglem4  42199  rpnnen3  43044
  Copyright terms: Public domain W3C validator