Theorem necon2ad 2434

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1373   ≠ wne 2377

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 2378

This theorem is referenced by:  necon2d  2436  prneimg  3817  tz7.2  4405  nordeq  4596  pr2ne  7307  ltne  8164  apne  8703  xrltne  9942  npnflt  9944  nmnfgt  9947  ge0nemnf  9953  rpexp  12519  sqrt2irr  12528  pcgcd1  12695  nzrunit  13994  lgsmod  15547