Theorem necon2bi 2988

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  rzalALT  4457  difsnb  4775  dtrucor2  5345  omeulem1  8568  kmlem6  10140  winainflem  10679  0npi  10868  0npr  10978  0nsr  11065  rexmul  13298  rennim  15292  mrissmrcd  17697  sdrgacs  20885  prmirred  21605  pthaus  23776  rplogsumlem2  27627  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  1div0apr  30797  bnj1311  35390  kardeq0  35547  subfacp1lem6  35655  bj-dtrucor2v  37430  itg2addnclem3  38302  cdleme31id  41146  rzalf  45717  jumpncnp  46592  fourierswlem  46924  pgnbgreunbgrlem2lem3  48858  pgnbgreunbgrlem5lem3  48864