Theorem necon2bi 2963

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  rzalALT  4436  difsnb  4750  dtrucor2  5307  omeulem1  8508  kmlem6  10067  winainflem  10605  0npi  10794  0npr  10904  0nsr  10991  1div0OLD  11799  rexmul  13212  rennim  15190  mrissmrcd  17595  sdrgacs  20767  prmirred  21462  pthaus  23612  rplogsumlem2  27467  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  1div0apr  30558  bnj1311  35187  subfacp1lem6  35388  bj-dtrucor2v  37137  itg2addnclem3  38005  cdleme31id  40851  rzalf  45463  jumpncnp  46341  fourierswlem  46673  pgnbgreunbgrlem2lem3  48589  pgnbgreunbgrlem5lem3  48595