Theorem necon2d 2956

Description: Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)

Hypothesis

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

Assertion

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

Proof of Theorem necon2d

Step	Hyp	Ref	Expression
1		necon2d.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷))
2		df-ne 2934	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	imbitrdi 251	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
4	3	necon2ad 2948	1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  map0g  8834  cantnf  9614  hashprg  14330  bcthlem5  25296  deg1ldgn  26066  cxpeq0  26655  lfgrn1cycl  29890  uspgrn2crct  29893  poimirlem17  37882  poimirlem20  37885  poimirlem22  37887  poimirlem27  37892  islshpat  39387  cdleme18b  40662  cdlemh  41187  prjspner1  42978