Theorem necon2bd 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon4bd  2953  necon4d  2957  minel  4420  disjiun  5088  eceqoveq  8771  en3lp  9535  infpssrlem5  10229  nneo  12588  zeo2  12591  sqrt2irr  16186  bezoutr1  16508  coprm  16650  dfphi2  16713  pltirr  18268  oddvdsnn0  19485  psgnodpmr  21557  supnfcls  23976  flimfnfcls  23984  metds0  24807  metdseq0  24811  metnrmlem1a  24815  sineq0  26501  lgsqr  27330  staddi  32333  stadd3i  32335  eulerpartlems  34537  erdszelem8  35411  finminlem  36531  ordcmp  36660  poimirlem18  37883  poimirlem21  37886  cvrnrefN  39652  trlnidatb  40547  flt4lem2  42999