Theorem necon2d 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  map0g  8923  cantnf  9731  hashprg  14431  bcthlem5  25376  deg1ldgn  26147  cxpeq0  26735  lfgrn1cycl  29835  uspgrn2crct  29838  poimirlem17  37624  poimirlem20  37627  poimirlem22  37629  poimirlem27  37634  islshpat  38999  cdleme18b  40275  cdlemh  40800  prjspner1  42613