Theorem necon1d 2845

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 2827	. . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷)
3	1, 2	syl6ibr 242	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷))
4	3	necon4ad 2842	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  disji  4669  mul02lem2  10251  xblss2ps  22253  xblss2  22254  lgsne0  25105  h1datomi  28568  eigorthi  28824  disjif  29517  lineintmo  32389  poimirlem6  33545  poimirlem7  33546  2llnmat  35128  2lnat  35388  tendospcanN  36629  dihmeetlem13N  36925  dochkrshp  36992