Theorem necon2bi 2973

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  rzalALT  4437  difsnb  4736  dtrucor2  5290  omeulem1  8375  kmlem6  9842  winainflem  10380  0npi  10569  0npr  10679  0nsr  10766  1div0  11564  rexmul  12934  rennim  14878  mrissmrcd  17266  sdrgacs  19984  prmirred  20608  pthaus  22697  rplogsumlem2  26538  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  1div0apr  28733  bnj1311  32904  subfacp1lem6  33047  bj-dtrucor2v  34927  itg2addnclem3  35757  cdleme31id  38335  rzalf  42449  jumpncnp  43329  fourierswlem  43661