Theorem necon2d 2980

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

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

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 2958

This theorem is used by:  map0g  8895  cantnf  9676  hashprg  14463  bcthlem5  25562  deg1ldgn  26325  cxpeq0  26923  lfgrn1cycl  30281  uspgrn2crct  30284  poimirlem17  38394  poimirlem20  38397  poimirlem22  38399  poimirlem27  38404  islshpat  39898  cdleme18b  41173  cdlemh  41698  prjspner1  43480