Theorem necon2bd 2976

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  necon4bd  2980  necon4d  2984  minel  4423  disjiun  5092  eceqoveq  8808  en3lp  9571  infpssrlem5  10279  nneo  12668  zeo2  12671  sqrt2irr  16293  bezoutr1  16615  coprm  16758  dfphi2  16821  pltirr  18377  oddvdsnn0  19602  psgnodpmr  21697  supnfcls  24134  flimfnfcls  24142  metds0  24965  metdseq0  24969  metnrmlem1a  24973  sineq0  26643  lgsqr  27469  staddi  32503  stadd3i  32505  eulerpartlems  34662  erdszelem8  35556  finminlem  36686  ordcmp  36815  poimirlem18  38144  poimirlem21  38147  cvrnrefN  39913  trlnidatb  40808  flt4lem2  43236