Theorem necon2bi 2974

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 2948	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
3	2	con2i 139	1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  rzalALT  4440  difsnb  4739  dtrucor2  5295  omeulem1  8413  kmlem6  9911  winainflem  10449  0npi  10638  0npr  10748  0nsr  10835  1div0  11634  rexmul  13005  rennim  14950  mrissmrcd  17349  sdrgacs  20069  prmirred  20696  pthaus  22789  rplogsumlem2  26633  pntrlog2bndlem4  26728  pntrlog2bndlem5  26729  1div0apr  28832  bnj1311  33004  subfacp1lem6  33147  bj-dtrucor2v  35000  itg2addnclem3  35830  cdleme31id  38408  rzalf  42560  jumpncnp  43439  fourierswlem  43771