Theorem necon2bi 2990

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1508   ≠ wne 2960

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 199  df-ne 2961

This theorem is referenced by:  rzal  4330  difsnb  4609  dtrucor2  5122  omeulem1  8007  kmlem6  9373  winainflem  9911  0npi  10100  0npr  10210  0nsr  10297  1div0  11098  rexmul  12478  rennim  14457  mrissmrcd  16781  sdrgacs  19314  prmirred  20359  pthaus  21965  rplogsumlem2  25778  pntrlog2bndlem4  25873  pntrlog2bndlem5  25874  1div0apr  28039  bnj1311  31973  subfacp1lem6  32054  bj-dtrucor2v  33666  itg2addnclem3  34423  cdleme31id  37012  rzalf  40731  jumpncnp  41645  fourierswlem  41980