Theorem necon3ai 2986

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

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

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 2962

This theorem is used by:  necon1ai  2988  necon3i  2993  neneor  3063  nelsn  4637  disjsn2  4683  prnesn  4830  opelopabsb  5519  funsndifnop  7155  ord1eln01  8490  map0b  8890  mapdom3  9147  cflim2  10265  isfin4p1  10317  fpwwe2lem12  10645  tskuni  10786  recextlem2  11863  hashprg  14451  eqsqrt2d  15446  gcd1  16611  gcdzeq  16635  lcmfunsnlem2lem1  16721  lcmfunsnlem2lem2  16722  phimullem  16863  pcgcd1  16962  pc2dvds  16964  pockthlem  16990  ablfacrplem  20168  znrrg  21752  opnfbas  24036  supfil  24089  itg1addlem4  25895  itg1addlem5  25896  mpodvdsmulf1o  27395  dvdsmulf1o  27397  ppiub  27405  dchrelbas4  27444  2sqlem8  27627  tgldimor  28808  subfacp1lem6  35698  cvmsss2  35787  ax6e2ndeq  45309  supminfxr2  46224  fourierdlem56  46917  ichnreuop  48262