Theorem necon2bi 2970

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

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

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 2940

This theorem is referenced by:  rzalALT  4509  difsnb  4809  dtrucor2  5370  omeulem1  8585  kmlem6  10153  winainflem  10691  0npi  10880  0npr  10990  0nsr  11077  1div0  11878  rexmul  13255  rennim  15191  mrissmrcd  17589  sdrgacs  20561  prmirred  21246  pthaus  23363  rplogsumlem2  27225  pntrlog2bndlem4  27320  pntrlog2bndlem5  27321  1div0apr  29989  bnj1311  34334  subfacp1lem6  34475  bj-dtrucor2v  35999  itg2addnclem3  36845  cdleme31id  39569  rzalf  44004  jumpncnp  44913  fourierswlem  45245