Theorem necon2bd 2958

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

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

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 2943

This theorem is referenced by:  necon4bd  2962  necon4d  2966  minel  4396  disjiun  5057  eceqoveq  8569  en3lp  9302  infpssrlem5  9994  nneo  12334  zeo2  12337  sqrt2irr  15886  bezoutr1  16202  coprm  16344  dfphi2  16403  pltirr  17968  oddvdsnn0  19067  psgnodpmr  20707  supnfcls  23079  flimfnfcls  23087  metds0  23919  metdseq0  23923  metnrmlem1a  23927  sineq0  25585  lgsqr  26404  staddi  30509  stadd3i  30511  eulerpartlems  32227  erdszelem8  33060  finminlem  34434  ordcmp  34563  poimirlem18  35722  poimirlem21  35725  cvrnrefN  37223  trlnidatb  38118  flt4lem2  40400