Theorem necon4d 2980

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 2972	. 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵))
3		nne 2960	. 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
4	2, 3	imbitrdi 254	1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  oa00  8560  map0g  8905  epfrs  9725  fin23lem24  10393  abs00  15449  oddvds  19754  01eq0ringOLD  20775  isdomn4  20960  isabvd  21062  uvcf1  22091  lindff1  22119  hausnei2  23664  dfconn2  23730  hausflimi  24292  hauspwpwf1  24299  cxpeq0  26999  his6  31694  fnpreimac  33257  deg1le0eq0  34098  lkreqN  40207  ltrnideq  41212  hdmapip0  42952  sticksstones2  43177  unitscyglem4  43228  rpnnen3  44018