Theorem necon2bd 2956

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  necon4bd  2960  necon4d  2964  minel  4466  disjiun  5131  eceqoveq  8862  en3lp  9654  infpssrlem5  10347  nneo  12702  zeo2  12705  sqrt2irr  16285  bezoutr1  16606  coprm  16748  dfphi2  16811  pltirr  18380  oddvdsnn0  19562  psgnodpmr  21608  supnfcls  24028  flimfnfcls  24036  metds0  24872  metdseq0  24876  metnrmlem1a  24880  sineq0  26566  lgsqr  27395  staddi  32265  stadd3i  32267  eulerpartlems  34362  erdszelem8  35203  finminlem  36319  ordcmp  36448  poimirlem18  37645  poimirlem21  37648  cvrnrefN  39283  trlnidatb  40179  flt4lem2  42657