Theorem necon2bi 2986

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  rzalALT  4451  difsnb  4769  dtrucor2  5334  omeulem1  8574  kmlem6  10215  winainflem  10759  0npi  10948  0npr  11058  0nsr  11145  rexmul  13382  rennim  15386  mrissmrcd  17794  zrdrng  21006  sdrgacs  21038  prmirred  21760  pthaus  23937  rplogsumlem2  27794  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  1div0apr  31051  bnj1311  35637  kardeq0  35797  subfacp1lem6  35919  bj-dtrucor2v  37699  itg2addnclem3  38559  cdleme31id  41419  rzalf  45977  jumpncnp  46852  fourierswlem  47184  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem5lem3  49164  crosspv2d  50905  crosspv3d  50906