Theorem necon3ai 2984

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

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

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 2960

This theorem is used by:  necon1ai  2986  necon3i  2991  neneor  3061  nelsn  4627  disjsn2  4673  prnesn  4818  opelopabsb  5509  funsndifnop  7182  ord1eln01  8535  map0b  8942  mapdom3  9199  isfin4p1  10423  fpwwe2lem12  10757  tskuni  10898  recextlem2  11977  hashprg  14569  eqsqrt2d  15568  gcd1  16733  gcdzeq  16757  lcmfunsnlem2lem1  16845  lcmfunsnlem2lem2  16846  phimullem  16988  pcgcd1  17087  pc2dvds  17089  pockthlem  17115  ablfacrplem  20314  znrrg  21904  opnfbas  24194  supfil  24247  itg1addlem4  26053  itg1addlem5  26054  mpodvdsmulf1o  27554  dvdsmulf1o  27556  ppiub  27564  dchrelbas4  27603  2sqlem8  27786  tgldimor  28998  subfacp1lem6  36130  cvmsss2  36219  ax6e2ndeq  45744  supminfxr2  46694  fourierdlem56  47387  ichnreuop  48769