Theorem necon2bi 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  rzalALT  4435  difsnb  4751  dtrucor2  5314  omeulem1  8517  kmlem6  10078  winainflem  10616  0npi  10805  0npr  10915  0nsr  11002  1div0OLD  11810  rexmul  13223  rennim  15201  mrissmrcd  17606  sdrgacs  20778  prmirred  21454  pthaus  23603  rplogsumlem2  27448  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  1div0apr  30538  bnj1311  35166  subfacp1lem6  35367  bj-dtrucor2v  37124  itg2addnclem3  37994  cdleme31id  40840  rzalf  45448  jumpncnp  46326  fourierswlem  46658  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem3  48598