Theorem necon2bi 2962

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

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

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 2933

This theorem is referenced by:  rzalALT  4485  difsnb  4782  dtrucor2  5342  omeulem1  8594  kmlem6  10170  winainflem  10707  0npi  10896  0npr  11006  0nsr  11093  1div0OLD  11897  rexmul  13287  rennim  15258  mrissmrcd  17652  sdrgacs  20761  prmirred  21435  pthaus  23576  rplogsumlem2  27448  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  1div0apr  30449  bnj1311  35055  subfacp1lem6  35207  bj-dtrucor2v  36835  itg2addnclem3  37697  cdleme31id  40413  rzalf  45041  jumpncnp  45927  fourierswlem  46259