Theorem necon2bd 2957

Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)

Hypothesis

Ref	Expression
necon2bd.1	⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Assertion

Ref	Expression
necon2bd	⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Proof of Theorem necon2bd

Step	Hyp	Ref	Expression
1		necon2bd.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))
2		df-ne 2942	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	imbitrdi 250	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
4	3	con2d 134	1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-ne 2942

This theorem is referenced by:  necon4bd  2961  necon4d  2965  minel  4466  disjiun  5136  eceqoveq  8816  en3lp  9609  infpssrlem5  10302  nneo  12646  zeo2  12649  sqrt2irr  16192  bezoutr1  16506  coprm  16648  dfphi2  16707  pltirr  18288  oddvdsnn0  19412  psgnodpmr  21143  supnfcls  23524  flimfnfcls  23532  metds0  24366  metdseq0  24370  metnrmlem1a  24374  sineq0  26033  lgsqr  26854  staddi  31499  stadd3i  31501  eulerpartlems  33359  erdszelem8  34189  finminlem  35203  ordcmp  35332  poimirlem18  36506  poimirlem21  36509  cvrnrefN  38152  trlnidatb  39048  flt4lem2  41389