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 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

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

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

This theorem is referenced by:  nelsn  3743  disjsn2  3771  0nelxp  4800  fvunsng  5903  map0b  6962  difinfsnlem  7433  hashprg  11232  gcd1  12747  gcdzeq  12782  phimullem  12986  pcgcd1  13090  pc2dvds  13092  pockthlem  13118  znrrg  14978  mpodvdsmulf1o  16087  2sqlem8  16225