Theorem necon1d 2978

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

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

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 2957

This theorem is used by:  disji  5088  mul02lem2  11468  mhpmulcl  22450  xblss2ps  24700  xblss2  24701  lgsne0  27644  h1datomi  32165  eigorthi  32421  disjif  33154  lineintmo  36892  poimirlem6  38512  poimirlem7  38513  2llnmat  40549  2lnat  40809  tendospcanN  42048  dihmeetlem13N  42344  dochkrshp  42411  remul02  43424  remul01  43426  sn-0tie0  43483  oppcthinendcALT  50493