Theorem necon2bd 2839

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 2824	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	syl6ib 241	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
4	3	con2d 129	1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon4bd  2843  necon4d  2847  minel  4066  disjiun  4672  eceqoveq  7895  en3lp  8551  infpssrlem5  9167  nneo  11499  zeo2  11502  sqrt2irr  15023  bezoutr1  15329  coprm  15470  dfphi2  15526  pltirr  17010  oddvdsnn0  18009  psgnodpmr  19984  supnfcls  21871  flimfnfcls  21879  metds0  22700  metdseq0  22704  metnrmlem1a  22708  sineq0  24318  lgsqr  25121  staddi  29233  stadd3i  29235  eulerpartlems  30550  erdszelem8  31306  finminlem  32437  ordcmp  32571  poimirlem18  33557  poimirlem21  33560  cvrnrefN  34887  trlnidatb  35782