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

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

This theorem is referenced by:  rzalALT  4452  difsnb  4769  dtrucor2  5334  omeulem1  8555  kmlem6  10127  winainflem  10666  0npi  10855  0npr  10965  0nsr  11052  rexmul  13288  rennim  15280  mrissmrcd  17686  sdrgacs  20873  prmirred  21584  pthaus  23756  rplogsumlem2  27607  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  1div0apr  30728  bnj1311  35329  subfacp1lem6  35548  bj-dtrucor2v  37314  itg2addnclem3  38184  cdleme31id  41030  rzalf  45595  jumpncnp  46470  fourierswlem  46802  pgnbgreunbgrlem2lem3  48736  pgnbgreunbgrlem5lem3  48742