Theorem necon2bi 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  rzalALT  4460  difsnb  4758  dtrucor2  5310  omeulem1  8497  kmlem6  10044  winainflem  10581  0npi  10770  0npr  10880  0nsr  10967  1div0OLD  11774  rexmul  13167  rennim  15143  mrissmrcd  17543  sdrgacs  20714  prmirred  21409  pthaus  23551  rplogsumlem2  27421  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  1div0apr  30443  bnj1311  35031  subfacp1lem6  35217  bj-dtrucor2v  36850  itg2addnclem3  37712  cdleme31id  40432  rzalf  45053  jumpncnp  45935  fourierswlem  46267  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem5lem3  48152