Theorem necon2bi 2973

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ≠ wne 2943

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 197  df-ne 2944

This theorem is referenced by:  rzal  4214  difsnb  4472  dtrucor2  5029  kmlem6  9179  winainflem  9717  0npi  9906  0npr  10016  0nsr  10102  1div0  10888  rexmul  12306  rennim  14187  mrissmrcd  16508  prmirred  20058  pthaus  21662  rplogsumlem2  25395  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  1div0apr  27666  bnj1311  31430  subfacp1lem6  31505  bj-dtrucor2v  33137  itg2addnclem3  33795  cdleme31id  36203  sdrgacs  38297  rzalf  39698  jumpncnp  40629  fourierswlem  40964