Theorem necon2bd 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon4bd  2949  necon4d  2953  minel  4415  disjiun  5081  eceqoveq  8752  en3lp  9511  infpssrlem5  10205  nneo  12563  zeo2  12566  sqrt2irr  16160  bezoutr1  16482  coprm  16624  dfphi2  16687  pltirr  18241  oddvdsnn0  19458  psgnodpmr  21529  supnfcls  23936  flimfnfcls  23944  metds0  24767  metdseq0  24771  metnrmlem1a  24775  sineq0  26461  lgsqr  27290  staddi  32228  stadd3i  32230  eulerpartlems  34394  erdszelem8  35263  finminlem  36383  ordcmp  36512  poimirlem18  37698  poimirlem21  37701  cvrnrefN  39401  trlnidatb  40296  flt4lem2  42765