Theorem necon2ad 2417

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 625	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
3		df-ne 2361	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 162	1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1364   ≠ wne 2360

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 615  ax-in2 616

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

This theorem is referenced by:  necon2d  2419  prneimg  3789  tz7.2  4372  nordeq  4561  pr2ne  7222  ltne  8073  apne  8611  xrltne  9845  npnflt  9847  nmnfgt  9850  ge0nemnf  9856  rpexp  12188  sqrt2irr  12197  pcgcd1  12363  nzrunit  13552  lgsmod  14905