Theorem necon4d 2956

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  oa00  8486  map0g  8822  epfrs  9640  fin23lem24  10232  abs00  15212  oddvds  19476  01eq0ringOLD  20464  isdomn4  20649  isabvd  20745  uvcf1  21747  lindff1  21775  hausnei2  23297  dfconn2  23363  hausflimi  23924  hauspwpwf1  23931  cxpeq0  26643  his6  31174  fnpreimac  32749  deg1le0eq0  33654  lkreqN  39426  ltrnideq  40431  hdmapip0  42171  sticksstones2  42397  unitscyglem4  42448  rpnnen3  43270