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 1541   ≠ 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  4418  disjiun  5086  eceqoveq  8759  en3lp  9523  infpssrlem5  10217  nneo  12576  zeo2  12579  sqrt2irr  16174  bezoutr1  16496  coprm  16638  dfphi2  16701  pltirr  18256  oddvdsnn0  19473  psgnodpmr  21545  supnfcls  23964  flimfnfcls  23972  metds0  24795  metdseq0  24799  metnrmlem1a  24803  sineq0  26489  lgsqr  27318  staddi  32321  stadd3i  32323  eulerpartlems  34517  erdszelem8  35392  finminlem  36512  ordcmp  36641  poimirlem18  37835  poimirlem21  37838  cvrnrefN  39538  trlnidatb  40433  flt4lem2  42886