Theorem necon2bd 2941

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  necon4bd  2945  necon4d  2949  minel  4429  disjiun  5095  eceqoveq  8795  en3lp  9567  infpssrlem5  10260  nneo  12618  zeo2  12621  sqrt2irr  16217  bezoutr1  16539  coprm  16681  dfphi2  16744  pltirr  18294  oddvdsnn0  19474  psgnodpmr  21499  supnfcls  23907  flimfnfcls  23915  metds0  24739  metdseq0  24743  metnrmlem1a  24747  sineq0  26433  lgsqr  27262  staddi  32175  stadd3i  32177  eulerpartlems  34351  erdszelem8  35185  finminlem  36306  ordcmp  36435  poimirlem18  37632  poimirlem21  37635  cvrnrefN  39275  trlnidatb  40171  flt4lem2  42635