Theorem necon2bi 2971

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 207  df-ne 2941

This theorem is referenced by:  rzalALT  4510  difsnb  4806  dtrucor2  5372  omeulem1  8620  kmlem6  10196  winainflem  10733  0npi  10922  0npr  11032  0nsr  11119  1div0OLD  11923  rexmul  13313  rennim  15278  mrissmrcd  17683  sdrgacs  20802  prmirred  21485  pthaus  23646  rplogsumlem2  27529  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  1div0apr  30487  bnj1311  35038  subfacp1lem6  35190  bj-dtrucor2v  36818  itg2addnclem3  37680  cdleme31id  40396  rzalf  45022  jumpncnp  45913  fourierswlem  46245