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

Theorem necon4d 2806
 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 2798 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2786 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3syl6ib 240 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  oa00  7526  map0g  7783  epfrs  8490  fin23lem24  9027  abs00  13877  oddvds  17789  isabvd  18643  01eq0ring  19093  uvcf1  19950  lindff1  19978  hausnei2  20967  dfcon2  21032  hausflimi  21594  hauspwpwf1  21601  cxpeq0  24224  his6  27340  nn0sqeq1  28901  lkreqN  33475  ltrnideq  34480  hdmapip0  36225  rpnnen3  36617
 Copyright terms: Public domain W3C validator