Theorem necon2bi 2989

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

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

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 2960

This theorem is used by:  rzalALT  4454  difsnb  4769  dtrucor2  5338  omeulem1  8618  kmlem6  10261  winainflem  10805  0npi  10994  0npr  11104  0nsr  11191  rexmul  13428  rennim  15435  mrissmrcd  17843  zrdrng  21056  sdrgacs  21088  prmirred  21810  pthaus  23987  rplogsumlem2  27842  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  1div0apr  31099  bnj1311  35724  kardeq0  35924  subfacp1lem6  36117  bj-dtrucor2v  37907  itg2addnclem3  38783  cdleme31id  41643  rzalf  46239  jumpncnp  47113  fourierswlem  47445  pgnbgreunbgrlem2lem3  49419  pgnbgreunbgrlem5lem3  49425  crosspv2d  51241  crosspv3d  51242