Theorem necon2bi 3046

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  rzal  4452  difsnb  4732  dtrucor2  5265  omeulem1  8202  kmlem6  9575  winainflem  10109  0npi  10298  0npr  10408  0nsr  10495  1div0  11293  rexmul  12658  rennim  14592  mrissmrcd  16905  sdrgacs  19574  prmirred  20636  pthaus  22240  rplogsumlem2  26055  pntrlog2bndlem4  26150  pntrlog2bndlem5  26151  1div0apr  28241  bnj1311  32291  subfacp1lem6  32427  bj-dtrucor2v  34135  itg2addnclem3  34939  cdleme31id  37524  rzalf  41267  jumpncnp  42174  fourierswlem  42509