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

Theorem necon4d 2965
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 2957 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2945 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3syl6ib 254 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1543  wne 2941
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 210  df-ne 2942
This theorem is referenced by:  oa00  8307  map0g  8585  epfrs  9371  fin23lem24  9960  abs00  14877  oddvds  18963  isabvd  19880  01eq0ring  20334  uvcf1  20778  lindff1  20806  hausnei2  22274  dfconn2  22340  hausflimi  22901  hauspwpwf1  22908  cxpeq0  25590  his6  29204  fnpreimac  30752  lkreqN  36947  ltrnideq  37952  hdmapip0  39692  sticksstones2  39854  isdomn4  39923  rpnnen3  40585
  Copyright terms: Public domain W3C validator