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 141	1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ≠ 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 210  df-ne 2941

This theorem is referenced by:  rzalALT  4421  difsnb  4719  dtrucor2  5265  omeulem1  8310  kmlem6  9769  winainflem  10307  0npi  10496  0npr  10606  0nsr  10693  1div0  11491  rexmul  12861  rennim  14802  mrissmrcd  17143  sdrgacs  19845  prmirred  20461  pthaus  22535  rplogsumlem2  26366  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  1div0apr  28551  bnj1311  32717  subfacp1lem6  32860  bj-dtrucor2v  34737  itg2addnclem3  35567  cdleme31id  38145  rzalf  42233  jumpncnp  43114  fourierswlem  43446