Theorem necon2bd 2972

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon4bd  2976  necon4d  2980  minel  4419  disjiun  5091  onelfvnef1  8449  eceqoveq  8843  en3lp  9615  infpssrlem5  10385  nneo  12783  zeo2  12786  sqrt2irr  16417  bezoutr1  16744  coprm  16887  dfphi2  16951  pltirr  18507  oddvdsnn0  19758  psgnodpmr  21896  supnfcls  24339  flimfnfcls  24347  metds0  25170  metdseq0  25174  metnrmlem1a  25178  sineq0  26852  lgsqr  27678  flt4lem2  27977  staddi  32848  stadd3i  32850  eulerpartlems  34992  erdszelem8  35963  finminlem  37106  ordcmp  37235  poimirlem18  38556  poimirlem21  38559  cvrnrefN  40339  trlnidatb  41234