Theorem necon2bi 2986

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  rzalALT  4448  difsnb  4765  dtrucor2  5328  omeulem1  8546  kmlem6  10109  winainflem  10648  0npi  10837  0npr  10947  0nsr  11034  rexmul  13271  rennim  15249  mrissmrcd  17655  sdrgacs  20830  prmirred  21506  pthaus  23678  rplogsumlem2  27526  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  1div0apr  30616  bnj1311  35283  subfacp1lem6  35499  bj-dtrucor2v  37266  itg2addnclem3  38136  cdleme31id  40982  rzalf  45561  jumpncnp  46436  fourierswlem  46768  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem5lem3  48708