Theorem necon2bd 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon4bd  2966  necon4d  2970  minel  4489  disjiun  5154  eceqoveq  8880  en3lp  9683  infpssrlem5  10376  nneo  12727  zeo2  12730  sqrt2irr  16297  bezoutr1  16616  coprm  16758  dfphi2  16821  pltirr  18405  oddvdsnn0  19586  psgnodpmr  21631  supnfcls  24049  flimfnfcls  24057  metds0  24891  metdseq0  24895  metnrmlem1a  24899  sineq0  26584  lgsqr  27413  staddi  32278  stadd3i  32280  eulerpartlems  34325  erdszelem8  35166  finminlem  36284  ordcmp  36413  poimirlem18  37598  poimirlem21  37601  cvrnrefN  39238  trlnidatb  40134  flt4lem2  42602