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

Theorem necon4d 2805
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 2797 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2785 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3syl6ib 239 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  oa00  7503  map0g  7760  epfrs  8467  fin23lem24  9004  abs00  13823  oddvds  17735  isabvd  18589  01eq0ring  19039  uvcf1  19892  lindff1  19920  hausnei2  20909  dfcon2  20974  hausflimi  21536  hauspwpwf1  21543  cxpeq0  24141  his6  27146  nn0sqeq1  28707  lkreqN  33271  ltrnideq  34276  hdmapip0  36021  rpnnen3  36413
  Copyright terms: Public domain W3C validator