Theorem necon4d 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 207  df-ne 2939

This theorem is referenced by:  oa00  8596  map0g  8923  epfrs  9769  fin23lem24  10360  abs00  15325  oddvds  19580  01eq0ringOLD  20548  isdomn4  20733  isabvd  20830  uvcf1  21830  lindff1  21858  hausnei2  23377  dfconn2  23443  hausflimi  24004  hauspwpwf1  24011  cxpeq0  26735  his6  31128  fnpreimac  32688  deg1le0eq0  33578  lkreqN  39152  ltrnideq  40158  hdmapip0  41898  sticksstones2  42129  unitscyglem4  42180  rpnnen3  43021