Theorem necon2bd 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2934

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 210  df-ne 2935

This theorem is referenced by:  necon4bd  2954  necon4d  2958  minel  4355  disjiun  5017  eceqoveq  8433  en3lp  9150  infpssrlem5  9807  nneo  12147  zeo2  12150  sqrt2irr  15694  bezoutr1  16010  coprm  16152  dfphi2  16211  pltirr  17689  oddvdsnn0  18790  psgnodpmr  20406  supnfcls  22771  flimfnfcls  22779  metds0  23602  metdseq0  23606  metnrmlem1a  23610  sineq0  25268  lgsqr  26087  staddi  30181  stadd3i  30183  eulerpartlems  31897  erdszelem8  32731  finminlem  34150  ordcmp  34279  poimirlem18  35438  poimirlem21  35441  cvrnrefN  36939  trlnidatb  37834  flt4lem2  40076