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  4419  disjiun  5083  eceqoveq  8756  en3lp  9529  infpssrlem5  10220  nneo  12578  zeo2  12581  sqrt2irr  16176  bezoutr1  16498  coprm  16640  dfphi2  16703  pltirr  18257  oddvdsnn0  19441  psgnodpmr  21515  supnfcls  23923  flimfnfcls  23931  metds0  24755  metdseq0  24759  metnrmlem1a  24763  sineq0  26449  lgsqr  27278  staddi  32208  stadd3i  32210  eulerpartlems  34327  erdszelem8  35170  finminlem  36291  ordcmp  36420  poimirlem18  37617  poimirlem21  37620  cvrnrefN  39260  trlnidatb  40156  flt4lem2  42620