Theorem necon2bi 2969

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

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

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 207  df-ne 2939

This theorem is referenced by:  rzalALT  4516  difsnb  4811  dtrucor2  5378  omeulem1  8619  kmlem6  10194  winainflem  10731  0npi  10920  0npr  11030  0nsr  11117  1div0OLD  11921  rexmul  13310  rennim  15275  mrissmrcd  17685  sdrgacs  20819  prmirred  21503  pthaus  23662  rplogsumlem2  27544  pntrlog2bndlem4  27639  pntrlog2bndlem5  27640  1div0apr  30497  bnj1311  35017  subfacp1lem6  35170  bj-dtrucor2v  36800  itg2addnclem3  37660  cdleme31id  40377  rzalf  44955  jumpncnp  45854  fourierswlem  46186