Theorem necon2bd 2972

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon4bd  2976  necon4d  2980  minel  4419  disjiun  5087  eceqoveq  8799  en3lp  9566  infpssrlem5  10261  nneo  12654  zeo2  12657  sqrt2irr  16264  bezoutr1  16586  coprm  16729  dfphi2  16792  pltirr  18348  oddvdsnn0  19567  psgnodpmr  21622  supnfcls  24060  flimfnfcls  24068  metds0  24891  metdseq0  24895  metnrmlem1a  24899  sineq0  26566  lgsqr  27392  staddi  32395  stadd3i  32397  eulerpartlems  34618  erdszelem8  35512  finminlem  36642  ordcmp  36771  poimirlem18  38101  poimirlem21  38104  cvrnrefN  39870  trlnidatb  40765  flt4lem2  43193