Theorem necon2bd 2971

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon4bd  2975  necon4d  2979  minel  4419  disjiun  5091  eceqoveq  8822  en3lp  9593  infpssrlem5  10309  nneo  12705  zeo2  12708  sqrt2irr  16337  bezoutr1  16659  coprm  16802  dfphi2  16865  pltirr  18421  oddvdsnn0  19671  psgnodpmr  21803  supnfcls  24246  flimfnfcls  24254  metds0  25077  metdseq0  25081  metnrmlem1a  25085  sineq0  26761  lgsqr  27587  staddi  32727  stadd3i  32729  eulerpartlems  34871  erdszelem8  35777  finminlem  36937  ordcmp  37066  poimirlem18  38387  poimirlem21  38390  cvrnrefN  40155  trlnidatb  41050  flt4lem2  43493