Theorem necon3ai 2449

Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)

Hypothesis

Ref	Expression
necon3ai.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
necon3ai	⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Proof of Theorem necon3ai

Step	Hyp	Ref	Expression
1		df-ne 2401	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3ai.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	con3i 635	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝜑)
4	1, 3	sylbi 121	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395   ≠ wne 2400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 617  ax-in2 618

This theorem depends on definitions:  df-bi 117  df-ne 2401

This theorem is referenced by:  nelsn  3701  disjsn2  3729  0nelxp  4747  fvunsng  5837  map0b  6842  difinfsnlem  7274  hashprg  11038  gcd1  12516  gcdzeq  12551  phimullem  12755  pcgcd1  12859  pc2dvds  12861  pockthlem  12887  znrrg  14632  mpodvdsmulf1o  15672  2sqlem8  15810