Theorem necon3ai 2968

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-ne 2944

This theorem is referenced by:  necon1ai  2971  necon3i  2976  neneor  3044  nelsn  4601  disjsn2  4648  prnesn  4790  opelopabsb  5443  funsndifnop  7023  ord1eln01  8326  map0b  8671  mapdom3  8936  cflim2  10019  isfin4p1  10071  fpwwe2lem12  10398  tskuni  10539  recextlem2  11606  hashprg  14110  eqsqrt2d  15080  gcd1  16235  gcdzeq  16262  lcmfunsnlem2lem1  16343  lcmfunsnlem2lem2  16344  phimullem  16480  pcgcd1  16578  pc2dvds  16580  pockthlem  16606  ablfacrplem  19668  znrrg  20773  opnfbas  22993  supfil  23046  itg1addlem4  24863  itg1addlem4OLD  24864  itg1addlem5  24865  dvdsmulf1o  26343  ppiub  26352  dchrelbas4  26391  2sqlem8  26574  tgldimor  26863  subfacp1lem6  33147  cvmsss2  33236  ax6e2ndeq  42179  supminfxr2  43009  fourierdlem56  43703  ichnreuop  44924