Theorem necon1d 2979

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 2961	. . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷)
3	1, 2	imbitrrdi 255	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷))
4	3	necon4ad 2976	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))

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

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 2958

This theorem is used by:  disji  5092  mul02lem2  11415  mhpmulcl  22383  xblss2ps  24633  xblss2  24634  lgsne0  27579  h1datomi  32070  eigorthi  32326  disjif  33059  lineintmo  36745  poimirlem6  38383  poimirlem7  38384  2llnmat  40405  2lnat  40665  tendospcanN  41904  dihmeetlem13N  42200  dochkrshp  42267  remul02  43288  remul01  43290  sn-0tie0  43347  oppcthinendcALT  50375