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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ 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 207  df-ne 2933

This theorem is referenced by:  necon4bd  2952  necon4d  2956  minel  4406  disjiun  5073  eceqoveq  8769  en3lp  9535  infpssrlem5  10229  nneo  12613  zeo2  12616  sqrt2irr  16216  bezoutr1  16538  coprm  16681  dfphi2  16744  pltirr  18299  oddvdsnn0  19519  psgnodpmr  21570  supnfcls  23985  flimfnfcls  23993  metds0  24816  metdseq0  24820  metnrmlem1a  24824  sineq0  26488  lgsqr  27314  staddi  32317  stadd3i  32319  eulerpartlems  34504  erdszelem8  35380  finminlem  36500  ordcmp  36629  poimirlem18  37959  poimirlem21  37962  cvrnrefN  39728  trlnidatb  40623  flt4lem2  43080