Theorem necon2bd 2798

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon4bd  2802  necon4d  2806  minel  3985  disjiun  4573  eceqoveq  7740  en3lp  8396  infpssrlem5  9012  nneo  11337  zeo2  11340  sqrt2irr  14817  bezoutr1  15120  coprm  15261  dfphi2  15317  pltirr  16786  oddvdsnn0  17786  psgnodpmr  19755  supnfcls  21634  flimfnfcls  21642  metds0  22461  metdseq0  22465  metnrmlem1a  22469  sineq0  24077  lgsqr  24876  staddi  28489  stadd3i  28491  eulerpartlems  29749  erdszelem8  30434  finminlem  31482  ordcmp  31616  poimirlem18  32597  poimirlem21  32600  cvrnrefN  33587  trlnidatb  34482