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  8760  en3lp  9524  infpssrlem5  10218  nneo  12602  zeo2  12605  sqrt2irr  16205  bezoutr1  16527  coprm  16670  dfphi2  16733  pltirr  18288  oddvdsnn0  19508  psgnodpmr  21578  supnfcls  23994  flimfnfcls  24002  metds0  24825  metdseq0  24829  metnrmlem1a  24833  sineq0  26504  lgsqr  27333  staddi  32337  stadd3i  32339  eulerpartlems  34525  erdszelem8  35401  finminlem  36521  ordcmp  36650  poimirlem18  37970  poimirlem21  37973  cvrnrefN  39739  trlnidatb  40634  flt4lem2  43091