Theorem necon2bi 2965

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  rzalALT  4430  difsnb  4746  dtrucor2  5308  omeulem1  8514  kmlem6  10076  winainflem  10614  0npi  10803  0npr  10913  0nsr  11000  1div0OLD  11808  rexmul  13221  rennim  15199  mrissmrcd  17604  sdrgacs  20780  prmirred  21456  pthaus  23628  rplogsumlem2  27473  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  1div0apr  30563  bnj1311  35213  subfacp1lem6  35420  bj-dtrucor2v  37177  itg2addnclem3  38047  cdleme31id  40893  rzalf  45472  jumpncnp  46348  fourierswlem  46680  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem5lem3  48620