Theorem necon3ai 2463

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398   ≠ wne 2414

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

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

This theorem is referenced by:  nelsn  3726  disjsn2  3754  0nelxp  4779  fvunsng  5880  map0b  6923  difinfsnlem  7392  hashprg  11181  gcd1  12691  gcdzeq  12726  phimullem  12930  pcgcd1  13034  pc2dvds  13036  pockthlem  13062  znrrg  14857  mpodvdsmulf1o  15907  2sqlem8  16045