MPE Home 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