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 250 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1541  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 206  df-ne 2941
This theorem is referenced by:  oa00  8561  map0g  8880  epfrs  9728  fin23lem24  10319  abs00  15240  oddvds  19456  01eq0ringOLD  20420  isabvd  20571  isdomn4  21118  uvcf1  21566  lindff1  21594  hausnei2  23077  dfconn2  23143  hausflimi  23704  hauspwpwf1  23711  cxpeq0  26410  his6  30607  fnpreimac  32151  deg1le0eq0  32917  lkreqN  38343  ltrnideq  39349  hdmapip0  41089  sticksstones2  41269  rpnnen3  42073
  Copyright terms: Public domain W3C validator