Theorem necon2bd 2974

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  necon4bd  2978  necon4d  2982  minel  4427  disjiun  5098  eceqoveq  8821  en3lp  9584  infpssrlem5  10292  nneo  12681  zeo2  12684  sqrt2irr  16306  bezoutr1  16628  coprm  16771  dfphi2  16834  pltirr  18390  oddvdsnn0  19615  psgnodpmr  21721  supnfcls  24158  flimfnfcls  24166  metds0  24989  metdseq0  24993  metnrmlem1a  24997  sineq0  26670  lgsqr  27496  staddi  32579  stadd3i  32581  eulerpartlems  34731  erdszelem8  35671  finminlem  36810  ordcmp  36939  poimirlem18  38270  poimirlem21  38273  cvrnrefN  40037  trlnidatb  40932  flt4lem2  43362