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 1569   ≠ 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  4418  disjiun  5090  onelfvnef1  8453  eceqoveq  8847  en3lp  9619  infpssrlem5  10389  nneo  12787  zeo2  12790  sqrt2irr  16423  bezoutr1  16750  coprm  16893  dfphi2  16957  pltirr  18513  oddvdsnn0  19764  psgnodpmr  21902  supnfcls  24345  flimfnfcls  24353  metds0  25176  metdseq0  25180  metnrmlem1a  25184  sineq0  26858  lgsqr  27684  flt4lem2  27983  staddi  32854  stadd3i  32856  eulerpartlems  35039  erdszelem8  36050  finminlem  37199  ordcmp  37328  poimirlem18  38650  poimirlem21  38653  cvrnrefN  40433  trlnidatb  41328