Theorem necon2bd 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon4bd  2953  necon4d  2957  minel  4407  disjiun  5074  eceqoveq  8762  en3lp  9526  infpssrlem5  10220  nneo  12604  zeo2  12607  sqrt2irr  16207  bezoutr1  16529  coprm  16672  dfphi2  16735  pltirr  18290  oddvdsnn0  19510  psgnodpmr  21580  supnfcls  23995  flimfnfcls  24003  metds0  24826  metdseq0  24830  metnrmlem1a  24834  sineq0  26501  lgsqr  27328  staddi  32332  stadd3i  32334  eulerpartlems  34520  erdszelem8  35396  finminlem  36516  ordcmp  36645  poimirlem18  37973  poimirlem21  37976  cvrnrefN  39742  trlnidatb  40637  flt4lem2  43094