Theorem necon4d 2982

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  oa00  8545  map0g  8883  epfrs  9701  fin23lem24  10307  abs00  15342  oddvds  19618  01eq0ringOLD  20616  isdomn4  20801  isabvd  20896  uvcf1  21923  lindff1  21951  hausnei2  23491  dfconn2  23557  hausflimi  24118  hauspwpwf1  24125  cxpeq0  26824  his6  31432  fnpreimac  32996  deg1le0eq0  33844  lkreqN  39925  ltrnideq  40930  hdmapip0  42670  sticksstones2  42895  unitscyglem4  42946  rpnnen3  43742