Theorem necon2bi 2969

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

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

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 2939

This theorem is referenced by:  rzalALT  4508  difsnb  4808  dtrucor2  5369  omeulem1  8584  kmlem6  10152  winainflem  10690  0npi  10879  0npr  10989  0nsr  11076  1div0  11877  rexmul  13254  rennim  15190  mrissmrcd  17588  sdrgacs  20560  prmirred  21245  pthaus  23362  rplogsumlem2  27224  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  1div0apr  29988  bnj1311  34333  subfacp1lem6  34474  bj-dtrucor2v  35998  itg2addnclem3  36844  cdleme31id  39568  rzalf  44003  jumpncnp  44912  fourierswlem  45244