Theorem necon2bi 2956

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

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

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 2927

This theorem is referenced by:  rzalALT  4476  difsnb  4773  dtrucor2  5330  omeulem1  8549  kmlem6  10116  winainflem  10653  0npi  10842  0npr  10952  0nsr  11039  1div0OLD  11845  rexmul  13238  rennim  15212  mrissmrcd  17608  sdrgacs  20717  prmirred  21391  pthaus  23532  rplogsumlem2  27403  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  1div0apr  30404  bnj1311  35021  subfacp1lem6  35179  bj-dtrucor2v  36812  itg2addnclem3  37674  cdleme31id  40395  rzalf  45018  jumpncnp  45903  fourierswlem  46235  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem3  48116