Theorem necon2d 2979

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  map0g  8896  cantnf  9678  hashprg  14519  bcthlem5  25629  deg1ldgn  26391  cxpeq0  26988  lfgrn1cycl  30376  uspgrn2crct  30379  poimirlem17  38523  poimirlem20  38526  poimirlem22  38528  poimirlem27  38533  islshpat  40042  cdleme18b  41317  cdlemh  41842  prjspner1  43616