Theorem necon3ai 2953

Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 28-Oct-2024.)

Hypothesis

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

Assertion

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

Proof of Theorem necon3ai

Step	Hyp	Ref	Expression
1		neneq 2934	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
2		necon3ai.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	nsyl 140	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 207  df-ne 2929

This theorem is referenced by:  necon1ai  2955  necon3i  2960  neneor  3028  nelsn  4619  disjsn2  4665  prnesn  4812  opelopabsb  5470  funsndifnop  7084  ord1eln01  8411  map0b  8807  mapdom3  9062  cflim2  10151  isfin4p1  10203  fpwwe2lem12  10530  tskuni  10671  recextlem2  11745  hashprg  14299  eqsqrt2d  15273  gcd1  16436  gcdzeq  16460  lcmfunsnlem2lem1  16546  lcmfunsnlem2lem2  16547  phimullem  16687  pcgcd1  16786  pc2dvds  16788  pockthlem  16814  ablfacrplem  19977  znrrg  21500  opnfbas  23755  supfil  23808  itg1addlem4  25625  itg1addlem5  25626  mpodvdsmulf1o  27129  dvdsmulf1o  27131  ppiub  27140  dchrelbas4  27179  2sqlem8  27362  tgldimor  28478  subfacp1lem6  35217  cvmsss2  35306  ax6e2ndeq  44591  supminfxr2  45506  fourierdlem56  46199  ichnreuop  47502