Theorem necon2bi 2977

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  rzalALT  4533  difsnb  4831  dtrucor2  5390  omeulem1  8638  kmlem6  10225  winainflem  10762  0npi  10951  0npr  11061  0nsr  11148  1div0OLD  11950  rexmul  13333  rennim  15288  mrissmrcd  17698  sdrgacs  20824  prmirred  21508  pthaus  23667  rplogsumlem2  27547  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  1div0apr  30500  bnj1311  35000  subfacp1lem6  35153  bj-dtrucor2v  36783  itg2addnclem3  37633  cdleme31id  40351  rzalf  44917  jumpncnp  45819  fourierswlem  46151