Theorem necon2bi 2987

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

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

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 2958

This theorem is used by:  rzalALT  4454  difsnb  4772  dtrucor2  5341  omeulem1  8573  kmlem6  10162  winainflem  10706  0npi  10895  0npr  11005  0nsr  11092  rexmul  13327  rennim  15330  mrissmrcd  17734  zrdrng  20941  sdrgacs  20973  prmirred  21693  pthaus  23870  rplogsumlem2  27729  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  1div0apr  30956  bnj1311  35541  kardeq0  35690  subfacp1lem6  35772  bj-dtrucor2v  37568  itg2addnclem3  38430  cdleme31id  41275  rzalf  45859  jumpncnp  46734  fourierswlem  47066  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem5lem3  49046  crosspv2d  50802  crosspv3d  50803