Theorem necon2bi 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  rzalALT  4463  difsnb  4760  dtrucor2  5314  omeulem1  8507  kmlem6  10069  winainflem  10606  0npi  10795  0npr  10905  0nsr  10992  1div0OLD  11798  rexmul  13191  rennim  15164  mrissmrcd  17564  sdrgacs  20704  prmirred  21399  pthaus  23541  rplogsumlem2  27412  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  1div0apr  30430  bnj1311  34990  subfacp1lem6  35157  bj-dtrucor2v  36790  itg2addnclem3  37652  cdleme31id  40373  rzalf  44995  jumpncnp  45880  fourierswlem  46212  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem5lem3  48107