Theorem necon2ad 2458

Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)

Hypothesis

Ref	Expression
necon2ad.1	⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Assertion

Ref	Expression
necon2ad	⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Proof of Theorem necon2ad

Step	Hyp	Ref	Expression
1		necon2ad.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
2	1	con2d 629	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
3		df-ne 2402	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 162	1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1397   ≠ wne 2401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-ne 2402

This theorem is referenced by:  necon2d  2460  prneimg  3858  tz7.2  4453  nordeq  4644  pr2ne  7402  ltne  8269  apne  8808  xrltne  10053  npnflt  10055  nmnfgt  10058  ge0nemnf  10064  rpexp  12748  sqrt2irr  12757  pcgcd1  12924  nzrunit  14226  lgsmod  15784