Theorem necon3d 2464

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  necon3i  2468  pm13.18  2501  ssn0  3566  suppssov1  6299  suppfnss  6497  suppssfvg  6503  nnmord  6790  findcard2  7193  findcard2s  7194  addn0nid  8702  nn0n0n1ge2  9720  xnegdi  10281  efne0  12463  divgcdcoprmex  12898  pceulem  13095  pcqmul  13104  pcqcl  13107  pcaddlem  13140  pcadd  13141  grpinvnz  13927  ringelnzr  14545  lmodfopne  14714  lmodindp1  14816  birthdaylem1g  16147  clwwlkccat  16764  clwwlknonel  16795