Theorem necon2d 2958

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 2936	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	imbitrdi 252	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷))
4	3	necon2ad 2950	1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  map0g  8829  cantnf  9612  hashprg  14355  bcthlem5  25320  deg1ldgn  26083  cxpeq0  26667  lfgrn1cycl  29898  uspgrn2crct  29901  poimirlem17  38011  poimirlem20  38014  poimirlem22  38016  poimirlem27  38021  islshpat  39516  cdleme18b  40791  cdlemh  41316  prjspner1  43083