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

Theorem necon4d 2967
 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 2959 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2947 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3syl6ib 241 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ≠ wne 2943 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 197  df-ne 2944 This theorem is referenced by:  oa00  7793  map0g  8050  epfrs  8771  fin23lem24  9346  abs00  14237  oddvds  18173  isabvd  19030  01eq0ring  19487  uvcf1  20348  lindff1  20376  hausnei2  21378  dfconn2  21443  hausflimi  22004  hauspwpwf1  22011  cxpeq0  24645  his6  28296  nn0sqeq1  29853  lkreqN  34979  ltrnideq  35984  hdmapip0  37725  rpnnen3  38125
 Copyright terms: Public domain W3C validator