Theorem necon3d 2445

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 2443	. 2 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵))
3		df-ne 2402	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 162	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1397   ≠ wne 2401

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 619  ax-in2 620

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

This theorem is referenced by:  necon3i  2449  pm13.18  2482  ssn0  3536  suppssfv  6236  suppssov1  6237  nnmord  6690  findcard2  7083  findcard2s  7084  addn0nid  8558  nn0n0n1ge2  9555  xnegdi  10108  efne0  12262  divgcdcoprmex  12697  pceulem  12890  pcqmul  12899  pcqcl  12902  pcaddlem  12935  pcadd  12936  grpinvnz  13677  ringelnzr  14225  lmodfopne  14364  lmodindp1  14466  clwwlkccat  16281  clwwlknonel  16312