Theorem necon3ai 2981

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon1ai  2983  necon3i  2988  neneor  3056  nelsn  4624  disjsn2  4670  prnesn  4817  opelopabsb  5499  funsndifnop  7130  ord1eln01  8460  map0b  8861  mapdom3  9117  cflim2  10217  isfin4p1  10269  fpwwe2lem12  10597  tskuni  10738  recextlem2  11815  hashprg  14405  eqsqrt2d  15379  gcd1  16545  gcdzeq  16569  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  phimullem  16797  pcgcd1  16896  pc2dvds  16898  pockthlem  16924  ablfacrplem  20090  znrrg  21597  opnfbas  23882  supfil  23935  itg1addlem4  25741  itg1addlem5  25742  mpodvdsmulf1o  27235  dvdsmulf1o  27237  ppiub  27245  dchrelbas4  27284  2sqlem8  27467  tgldimor  28648  subfacp1lem6  35499  cvmsss2  35588  ax6e2ndeq  45099  supminfxr2  46007  fourierdlem56  46700  ichnreuop  48042