Theorem necon2bi 2991

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

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

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 2962

This theorem is used by:  rzalALT  4461  difsnb  4779  dtrucor2  5348  omeulem1  8576  kmlem6  10158  winainflem  10696  0npi  10885  0npr  10995  0nsr  11082  rexmul  13315  rennim  15316  mrissmrcd  17721  zrdrng  20909  sdrgacs  20941  prmirred  21661  pthaus  23832  rplogsumlem2  27686  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  1div0apr  30856  bnj1311  35444  kardeq0  35593  subfacp1lem6  35698  bj-dtrucor2v  37493  itg2addnclem3  38365  cdleme31id  41209  rzalf  45778  jumpncnp  46653  fourierswlem  46985  pgnbgreunbgrlem2lem3  48922  pgnbgreunbgrlem5lem3  48928  crosspv2i  50684  crosspv3i  50685