Theorem necon2bd 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2932

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 206  df-ne 2933

This theorem is referenced by:  necon4bd  2952  necon4d  2956  minel  4458  disjiun  5126  eceqoveq  8813  en3lp  9606  infpssrlem5  10299  nneo  12644  zeo2  12647  sqrt2irr  16191  bezoutr1  16505  coprm  16647  dfphi2  16708  pltirr  18292  oddvdsnn0  19456  psgnodpmr  21453  supnfcls  23848  flimfnfcls  23856  metds0  24690  metdseq0  24694  metnrmlem1a  24698  sineq0  26377  lgsqr  27203  staddi  31971  stadd3i  31973  eulerpartlems  33851  erdszelem8  34680  finminlem  35694  ordcmp  35823  poimirlem18  37000  poimirlem21  37003  cvrnrefN  38646  trlnidatb  39542  flt4lem2  41903