Theorem necon2bi 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  rzalALT  4473  difsnb  4770  dtrucor2  5327  omeulem1  8546  kmlem6  10109  winainflem  10646  0npi  10835  0npr  10945  0nsr  11032  1div0OLD  11838  rexmul  13231  rennim  15205  mrissmrcd  17601  sdrgacs  20710  prmirred  21384  pthaus  23525  rplogsumlem2  27396  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  1div0apr  30397  bnj1311  35014  subfacp1lem6  35172  bj-dtrucor2v  36805  itg2addnclem3  37667  cdleme31id  40388  rzalf  45011  jumpncnp  45896  fourierswlem  46228  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem3  48112