Theorem necon2bd 2944

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

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

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 207  df-ne 2929

This theorem is referenced by:  necon4bd  2948  necon4d  2952  minel  4416  disjiun  5079  eceqoveq  8746  en3lp  9504  infpssrlem5  10195  nneo  12554  zeo2  12557  sqrt2irr  16155  bezoutr1  16477  coprm  16619  dfphi2  16682  pltirr  18236  oddvdsnn0  19454  psgnodpmr  21525  supnfcls  23933  flimfnfcls  23941  metds0  24764  metdseq0  24768  metnrmlem1a  24772  sineq0  26458  lgsqr  27287  staddi  32221  stadd3i  32223  eulerpartlems  34368  erdszelem8  35230  finminlem  36351  ordcmp  36480  poimirlem18  37677  poimirlem21  37680  cvrnrefN  39320  trlnidatb  40215  flt4lem2  42679