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

Theorem necon4d 2847
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 2839 . 2 (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴𝐵))
3 nne 2827 . 2 𝐴𝐵𝐴 = 𝐵)
42, 3syl6ib 241 1 (𝜑 → (𝐶 = 𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  oa00  7684  map0g  7939  epfrs  8645  fin23lem24  9182  abs00  14073  oddvds  18012  isabvd  18868  01eq0ring  19320  uvcf1  20179  lindff1  20207  hausnei2  21205  dfconn2  21270  hausflimi  21831  hauspwpwf1  21838  cxpeq0  24469  his6  28084  nn0sqeq1  29641  lkreqN  34775  ltrnideq  35780  hdmapip0  37524  rpnnen3  37916
  Copyright terms: Public domain W3C validator