Theorem necon2bd 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 2944

This theorem is referenced by:  necon4bd  2963  necon4d  2967  minel  4399  disjiun  5061  eceqoveq  8611  en3lp  9372  infpssrlem5  10063  nneo  12404  zeo2  12407  sqrt2irr  15958  bezoutr1  16274  coprm  16416  dfphi2  16475  pltirr  18053  oddvdsnn0  19152  psgnodpmr  20795  supnfcls  23171  flimfnfcls  23179  metds0  24013  metdseq0  24017  metnrmlem1a  24021  sineq0  25680  lgsqr  26499  staddi  30608  stadd3i  30610  eulerpartlems  32327  erdszelem8  33160  finminlem  34507  ordcmp  34636  poimirlem18  35795  poimirlem21  35798  cvrnrefN  37296  trlnidatb  38191  flt4lem2  40484