Theorem necon4d 2979

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

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

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 2956

This theorem is used by:  oa00  8571  map0g  8916  epfrs  9736  fin23lem24  10404  abs00  15462  oddvds  19767  01eq0ringOLD  20788  isdomn4  20973  isabvd  21075  uvcf1  22104  lindff1  22132  hausnei2  23677  dfconn2  23743  hausflimi  24305  hauspwpwf1  24312  cxpeq0  27012  his6  31707  fnpreimac  33312  deg1le0eq0  34152  lkreqN  40321  ltrnideq  41326  hdmapip0  43066  sticksstones2  43291  unitscyglem4  43342  rpnnen3  44133