Theorem necon3ai 2469

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 2421	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3ai.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	con3i 641	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝜑)
4	1, 3	sylbi 121	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  nelsn  3744  disjsn2  3772  0nelxp  4804  fvunsng  5912  map0b  6972  difinfsnlem  7446  hashprg  11272  gcd1  12790  gcdzeq  12825  phimullem  13033  pcgcd1  13137  pc2dvds  13139  pockthlem  13165  znrrg  15105  mpodvdsmulf1o  16296  ppiqub  16305  2sqlem8  16459