Theorem necon4d 2983

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

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

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 2960

This theorem is used by:  oa00  8605  map0g  8950  epfrs  9769  fin23lem24  10439  abs00  15499  oddvds  19812  01eq0ringOLD  20833  isdomn4  21018  isabvd  21120  uvcf1  22153  lindff1  22181  hausnei2  23726  dfconn2  23792  hausflimi  24354  hauspwpwf1  24361  cxpeq0  27063  his6  31758  fnpreimac  33362  deg1le0eq0  34208  lkreqN  40493  ltrnideq  41498  hdmapip0  43238  sticksstones2  43463  unitscyglem4  43514  rpnnen3  44305