Theorem necon1d 2958

Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon1d.1	⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))

Assertion

Ref	Expression
necon1d	⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))

Proof of Theorem necon1d

Step	Hyp	Ref	Expression
1		necon1d.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))
2		nne 2940	. . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷)
3	1, 2	imbitrrdi 254	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷))
4	3	necon4ad 2955	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1548   ≠ wne 2936

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 209  df-ne 2937

This theorem is referenced by:  disji  5060  mul02lem2  11318  mhpmulcl  22141  xblss2ps  24388  xblss2  24389  lgsne0  27320  h1datomi  31674  eigorthi  31930  disjif  32671  lineintmo  36400  poimirlem6  38008  poimirlem7  38009  2llnmat  40031  2lnat  40291  tendospcanN  41530  dihmeetlem13N  41826  dochkrshp  41893  remul02  42897  remul01  42899  sn-0tie0  42956  oppcthinendcALT  49945