Theorem necon2bi 3046

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  rzal  4439  difsnb  4725  dtrucor2  5259  omeulem1  8194  kmlem6  9567  winainflem  10101  0npi  10290  0npr  10400  0nsr  10487  1div0  11285  rexmul  12651  rennim  14583  mrissmrcd  16894  sdrgacs  19563  prmirred  20625  pthaus  22229  rplogsumlem2  26047  pntrlog2bndlem4  26142  pntrlog2bndlem5  26143  1div0apr  28231  bnj1311  32303  subfacp1lem6  32439  bj-dtrucor2v  34147  itg2addnclem3  34979  cdleme31id  37562  rzalf  41364  jumpncnp  42271  fourierswlem  42605