Theorem necon2bd 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon4bd  2955  necon4d  2959  minel  4401  disjiun  5067  eceqoveq  8766  en3lp  9533  infpssrlem5  10227  nneo  12611  zeo2  12614  sqrt2irr  16214  bezoutr1  16536  coprm  16679  dfphi2  16742  pltirr  18297  oddvdsnn0  19517  psgnodpmr  21572  supnfcls  24010  flimfnfcls  24018  metds0  24841  metdseq0  24845  metnrmlem1a  24849  sineq0  26513  lgsqr  27339  staddi  32342  stadd3i  32344  eulerpartlems  34551  erdszelem8  35433  finminlem  36553  ordcmp  36682  poimirlem18  38012  poimirlem21  38015  cvrnrefN  39781  trlnidatb  40676  flt4lem2  43104