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 1541   ≠ 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  4448  difsnb  4762  dtrucor2  5317  omeulem1  8509  kmlem6  10066  winainflem  10604  0npi  10793  0npr  10903  0nsr  10990  1div0OLD  11797  rexmul  13186  rennim  15162  mrissmrcd  17563  sdrgacs  20734  prmirred  21429  pthaus  23582  rplogsumlem2  27452  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  1div0apr  30543  bnj1311  35180  subfacp1lem6  35379  bj-dtrucor2v  37018  itg2addnclem3  37870  cdleme31id  40650  rzalf  45258  jumpncnp  46138  fourierswlem  46470  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem5lem3  48364