Theorem necon4d 2962

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

Step	Hyp	Ref	Expression
1		necon4d.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))
2	1	necon2bd 2954	. 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵))
3		nne 2942	. 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
4	2, 3	imbitrdi 250	1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  oa00  8561  map0g  8880  epfrs  9728  fin23lem24  10319  abs00  15240  oddvds  19456  01eq0ringOLD  20420  isabvd  20571  isdomn4  21118  uvcf1  21566  lindff1  21594  hausnei2  23077  dfconn2  23143  hausflimi  23704  hauspwpwf1  23711  cxpeq0  26422  his6  30619  fnpreimac  32163  deg1le0eq0  32929  lkreqN  38343  ltrnideq  39349  hdmapip0  41089  sticksstones2  41269  rpnnen3  42073