Theorem necon1d 2977

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

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

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 2956

This theorem is used by:  disji  5087  mul02lem2  11490  mhpmulcl  22475  xblss2ps  24725  xblss2  24726  lgsne0  27667  h1datomi  32188  eigorthi  32444  disjif  33219  lineintmo  37014  poimirlem6  38637  poimirlem7  38638  2llnmat  40674  2lnat  40934  tendospcanN  42173  dihmeetlem13N  42469  dochkrshp  42536  remul02  43549  remul01  43551  sn-0tie0  43608  oppcthinendcALT  50669