Theorem necon2bi 2971

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940

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 2941

This theorem is referenced by:  rzalALT  4508  difsnb  4808  dtrucor2  5369  omeulem1  8578  kmlem6  10146  winainflem  10684  0npi  10873  0npr  10983  0nsr  11070  1div0  11869  rexmul  13246  rennim  15182  mrissmrcd  17580  sdrgacs  20409  prmirred  21035  pthaus  23133  rplogsumlem2  26977  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  1div0apr  29710  bnj1311  34023  subfacp1lem6  34164  bj-dtrucor2v  35683  itg2addnclem3  36529  cdleme31id  39253  rzalf  43686  jumpncnp  44600  fourierswlem  44932