Theorem necon2bi 2821

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1481   ≠ wne 2791

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 197  df-ne 2792

This theorem is referenced by:  minelOLD  4025  rzal  4064  difsnb  4328  dtrucor2  4892  kmlem6  8962  winainflem  9500  0npi  9689  0npr  9799  0nsr  9885  1div0  10671  rexmul  12086  rennim  13960  mrissmrcd  16281  prmirred  19824  pthaus  21422  rplogsumlem2  25155  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  numclwwlkffin0  27187  1div0apr  27294  bnj1311  31066  subfacp1lem6  31141  bj-dtrucor2v  32776  itg2addnclem3  33434  cdleme31id  35501  sdrgacs  37590  rzalf  38996  jumpncnp  39874  fourierswlem  40210