Theorem necon4d 2967

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 2959	. 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵))
3		nne 2947	. 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
4	2, 3	syl6ib 250	1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵))

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

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 2944

This theorem is referenced by:  oa00  8390  map0g  8672  epfrs  9489  fin23lem24  10078  abs00  15001  oddvds  19155  isabvd  20080  01eq0ring  20543  uvcf1  20999  lindff1  21027  hausnei2  22504  dfconn2  22570  hausflimi  23131  hauspwpwf1  23138  cxpeq0  25833  his6  29461  fnpreimac  31008  lkreqN  37184  ltrnideq  38189  hdmapip0  39929  sticksstones2  40103  isdomn4  40172  rpnnen3  40854