Theorem necon3ai 2981

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 2962	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
2		necon3ai.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	nsyl 141	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon1ai  2983  necon3i  2988  neneor  3058  nelsn  4627  disjsn2  4673  prnesn  4820  opelopabsb  5504  funsndifnop  7147  ord1eln01  8488  map0b  8895  mapdom3  9152  cflim2  10322  isfin4p1  10374  fpwwe2lem12  10708  tskuni  10849  recextlem2  11928  hashprg  14519  eqsqrt2d  15516  gcd1  16681  gcdzeq  16705  lcmfunsnlem2lem1  16793  lcmfunsnlem2lem2  16794  phimullem  16936  pcgcd1  17035  pc2dvds  17037  pockthlem  17063  ablfacrplem  20261  znrrg  21851  opnfbas  24141  supfil  24194  itg1addlem4  26000  itg1addlem5  26001  mpodvdsmulf1o  27503  dvdsmulf1o  27505  ppiub  27513  dchrelbas4  27552  2sqlem8  27735  tgldimor  28947  subfacp1lem6  35919  cvmsss2  36008  ax6e2ndeq  45501  supminfxr2  46423  fourierdlem56  47116  ichnreuop  48498