Theorem necon2bi 2959

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

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

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 2930

This theorem is referenced by:  rzalALT  4459  difsnb  4757  dtrucor2  5312  omeulem1  8503  kmlem6  10054  winainflem  10591  0npi  10780  0npr  10890  0nsr  10977  1div0OLD  11784  rexmul  13172  rennim  15148  mrissmrcd  17548  sdrgacs  20718  prmirred  21413  pthaus  23554  rplogsumlem2  27424  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  1div0apr  30450  bnj1311  35057  subfacp1lem6  35250  bj-dtrucor2v  36882  itg2addnclem3  37733  cdleme31id  40513  rzalf  45138  jumpncnp  46020  fourierswlem  46352  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem5lem3  48246