Theorem necon2bd 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  necon4bd  2952  necon4d  2956  minel  4441  disjiun  5107  eceqoveq  8836  en3lp  9628  infpssrlem5  10321  nneo  12677  zeo2  12680  sqrt2irr  16267  bezoutr1  16588  coprm  16730  dfphi2  16793  pltirr  18345  oddvdsnn0  19525  psgnodpmr  21550  supnfcls  23958  flimfnfcls  23966  metds0  24790  metdseq0  24794  metnrmlem1a  24798  sineq0  26485  lgsqr  27314  staddi  32227  stadd3i  32229  eulerpartlems  34392  erdszelem8  35220  finminlem  36336  ordcmp  36465  poimirlem18  37662  poimirlem21  37665  cvrnrefN  39300  trlnidatb  40196  flt4lem2  42670