Theorem necon3ai 2982

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

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

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 2958

This theorem is used by:  necon1ai  2984  necon3i  2989  neneor  3059  nelsn  4630  disjsn2  4676  prnesn  4823  opelopabsb  5512  funsndifnop  7152  ord1eln01  8487  map0b  8894  mapdom3  9151  cflim2  10269  isfin4p1  10321  fpwwe2lem12  10655  tskuni  10796  recextlem2  11873  hashprg  14463  eqsqrt2d  15460  gcd1  16624  gcdzeq  16648  lcmfunsnlem2lem1  16734  lcmfunsnlem2lem2  16735  phimullem  16876  pcgcd1  16975  pc2dvds  16977  pockthlem  17003  ablfacrplem  20200  znrrg  21784  opnfbas  24074  supfil  24127  itg1addlem4  25933  itg1addlem5  25934  mpodvdsmulf1o  27438  dvdsmulf1o  27440  ppiub  27448  dchrelbas4  27487  2sqlem8  27670  tgldimor  28852  subfacp1lem6  35772  cvmsss2  35861  ax6e2ndeq  45390  supminfxr2  46305  fourierdlem56  46998  ichnreuop  48380