Theorem necon2bi 2985

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  rzalALT  4450  difsnb  4765  dtrucor2  5333  omeulem1  8593  kmlem6  10237  winainflem  10781  0npi  10970  0npr  11080  0nsr  11167  rexmul  13404  rennim  15411  mrissmrcd  17819  zrdrng  21031  sdrgacs  21063  prmirred  21785  pthaus  23962  rplogsumlem2  27817  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  1div0apr  31074  bnj1311  35700  kardeq0  35880  subfacp1lem6  36036  bj-dtrucor2v  37821  itg2addnclem3  38684  cdleme31id  41544  rzalf  46127  jumpncnp  47001  fourierswlem  47333  pgnbgreunbgrlem2lem3  49307  pgnbgreunbgrlem5lem3  49313  crosspv2d  51129  crosspv3d  51130