Theorem necon2ad 2424

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

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

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 2368

This theorem is referenced by:  necon2d  2426  prneimg  3805  tz7.2  4390  nordeq  4581  pr2ne  7273  ltne  8130  apne  8669  xrltne  9907  npnflt  9909  nmnfgt  9912  ge0nemnf  9918  rpexp  12348  sqrt2irr  12357  pcgcd1  12524  nzrunit  13822  lgsmod  15353