Theorem necon2bi 2963

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)

Hypothesis

Ref	Expression
necon2bi.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
necon2bi	⊢ (𝐴 = 𝐵 → ¬ 𝜑)

Proof of Theorem necon2bi

Step	Hyp	Ref	Expression
1		necon2bi.1	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2	1	neneqd 2938	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
3	2	con2i 139	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:  rzalALT  4450  difsnb  4764  dtrucor2  5319  omeulem1  8519  kmlem6  10078  winainflem  10616  0npi  10805  0npr  10915  0nsr  11002  1div0OLD  11809  rexmul  13198  rennim  15174  mrissmrcd  17575  sdrgacs  20746  prmirred  21441  pthaus  23594  rplogsumlem2  27464  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  1div0apr  30555  bnj1311  35199  subfacp1lem6  35398  bj-dtrucor2v  37059  itg2addnclem3  37918  cdleme31id  40764  rzalf  45371  jumpncnp  46250  fourierswlem  46582  pgnbgreunbgrlem2lem3  48470  pgnbgreunbgrlem5lem3  48476