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  5309  omeulem1  8510  kmlem6  10069  winainflem  10607  0npi  10796  0npr  10906  0nsr  10993  1div0OLD  11801  rexmul  13214  rennim  15192  mrissmrcd  17597  sdrgacs  20769  prmirred  21464  pthaus  23613  rplogsumlem2  27462  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  1div0apr  30553  bnj1311  35182  subfacp1lem6  35383  bj-dtrucor2v  37140  itg2addnclem3  38008  cdleme31id  40854  rzalf  45466  jumpncnp  46344  fourierswlem  46676  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem5lem3  48610