Theorem necon3d 2444

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395   ≠ wne 2400

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 617  ax-in2 618

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

This theorem is referenced by:  necon3i  2448  pm13.18  2481  ssn0  3535  suppssfv  6226  suppssov1  6227  nnmord  6680  findcard2  7073  findcard2s  7074  addn0nid  8546  nn0n0n1ge2  9543  xnegdi  10096  efne0  12232  divgcdcoprmex  12667  pceulem  12860  pcqmul  12869  pcqcl  12872  pcaddlem  12905  pcadd  12906  grpinvnz  13647  ringelnzr  14194  lmodfopne  14333  lmodindp1  14435  clwwlkccat  16210  clwwlknonel  16241