Theorem necon3d 2408

Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem necon3d

Step	Hyp	Ref	Expression
1		necon3d.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))
2	1	necon3ad 2406	. 2 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵))
3		df-ne 2365	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 162	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1364   ≠ wne 2364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117  df-ne 2365

This theorem is referenced by:  necon3i  2412  pm13.18  2445  ssn0  3489  suppssfv  6126  suppssov1  6127  nnmord  6570  findcard2  6945  findcard2s  6946  addn0nid  8393  nn0n0n1ge2  9387  xnegdi  9934  efne0  11821  divgcdcoprmex  12240  pceulem  12432  pcqmul  12441  pcqcl  12444  pcaddlem  12477  pcadd  12478  grpinvnz  13143  ringelnzr  13683  lmodfopne  13822  lmodindp1  13924