Theorem necon2bd 2956

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 2941	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	imbitrdi 250	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
4	3	con2d 134	1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940

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 2941

This theorem is referenced by:  necon4bd  2960  necon4d  2964  minel  4465  disjiun  5135  eceqoveq  8818  en3lp  9611  infpssrlem5  10304  nneo  12648  zeo2  12651  sqrt2irr  16194  bezoutr1  16508  coprm  16650  dfphi2  16709  pltirr  18290  oddvdsnn0  19414  psgnodpmr  21149  supnfcls  23531  flimfnfcls  23539  metds0  24373  metdseq0  24377  metnrmlem1a  24381  sineq0  26040  lgsqr  26861  staddi  31537  stadd3i  31539  eulerpartlems  33428  erdszelem8  34258  finminlem  35289  ordcmp  35418  poimirlem18  36592  poimirlem21  36595  cvrnrefN  38238  trlnidatb  39134  flt4lem2  41471