Theorem necon3ai 2980

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

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

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 2956

This theorem is used by:  necon1ai  2982  necon3i  2987  neneor  3057  nelsn  4623  disjsn2  4669  prnesn  4814  opelopabsb  5503  funsndifnop  7155  ord1eln01  8507  map0b  8914  mapdom3  9171  isfin4p1  10396  fpwwe2lem12  10730  tskuni  10871  recextlem2  11950  hashprg  14542  eqsqrt2d  15541  gcd1  16706  gcdzeq  16730  lcmfunsnlem2lem1  16818  lcmfunsnlem2lem2  16819  phimullem  16961  pcgcd1  17060  pc2dvds  17062  pockthlem  17088  ablfacrplem  20286  znrrg  21876  opnfbas  24166  supfil  24219  itg1addlem4  26025  itg1addlem5  26026  mpodvdsmulf1o  27526  dvdsmulf1o  27528  ppiub  27536  dchrelbas4  27575  2sqlem8  27758  tgldimor  28970  subfacp1lem6  36036  cvmsss2  36125  ax6e2ndeq  45635  supminfxr2  46572  fourierdlem56  47265  ichnreuop  48647