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  5093  eceqoveq  8808  en3lp  9571  infpssrlem5  10279  nneo  12671  zeo2  12674  sqrt2irr  16295  bezoutr1  16617  coprm  16760  dfphi2  16823  pltirr  18379  oddvdsnn0  19605  psgnodpmr  21700  supnfcls  24138  flimfnfcls  24146  metds0  24969  metdseq0  24973  metnrmlem1a  24977  sineq0  26647  lgsqr  27473  staddi  32507  stadd3i  32509  eulerpartlems  34667  erdszelem8  35561  finminlem  36691  ordcmp  36820  poimirlem18  38149  poimirlem21  38152  cvrnrefN  39918  trlnidatb  40813  flt4lem2  43241