Theorem necon2bd 2942

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

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

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 2927

This theorem is referenced by:  necon4bd  2946  necon4d  2950  minel  4432  disjiun  5098  eceqoveq  8798  en3lp  9574  infpssrlem5  10267  nneo  12625  zeo2  12628  sqrt2irr  16224  bezoutr1  16546  coprm  16688  dfphi2  16751  pltirr  18301  oddvdsnn0  19481  psgnodpmr  21506  supnfcls  23914  flimfnfcls  23922  metds0  24746  metdseq0  24750  metnrmlem1a  24754  sineq0  26440  lgsqr  27269  staddi  32182  stadd3i  32184  eulerpartlems  34358  erdszelem8  35192  finminlem  36313  ordcmp  36442  poimirlem18  37639  poimirlem21  37642  cvrnrefN  39282  trlnidatb  40178  flt4lem2  42642