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

Theorem necon4d 2995
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 2987 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2975 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3syl6ib 243 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1653  wne 2971
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 199  df-ne 2972
This theorem is referenced by:  oa00  7879  map0g  8136  epfrs  8857  fin23lem24  9432  abs00  14370  oddvds  18279  isabvd  19138  01eq0ring  19595  uvcf1  20456  lindff1  20484  hausnei2  21486  dfconn2  21551  hausflimi  22112  hauspwpwf1  22119  cxpeq0  24765  his6  28481  nn0sqeq1  30031  lkreqN  35191  ltrnideq  36196  hdmapip0  37936  rpnnen3  38384
  Copyright terms: Public domain W3C validator