Theorem necon3ai 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  necon1ai  2959  necon3i  2964  neneor  3032  nelsn  4623  disjsn2  4669  prnesn  4816  opelopabsb  5478  funsndifnop  7096  ord1eln01  8423  map0b  8821  mapdom3  9077  cflim2  10173  isfin4p1  10225  fpwwe2lem12  10553  tskuni  10694  recextlem2  11768  hashprg  14318  eqsqrt2d  15292  gcd1  16455  gcdzeq  16479  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  phimullem  16706  pcgcd1  16805  pc2dvds  16807  pockthlem  16833  ablfacrplem  19996  znrrg  21520  opnfbas  23786  supfil  23839  itg1addlem4  25656  itg1addlem5  25657  mpodvdsmulf1o  27160  dvdsmulf1o  27162  ppiub  27171  dchrelbas4  27210  2sqlem8  27393  tgldimor  28574  subfacp1lem6  35379  cvmsss2  35468  ax6e2ndeq  44796  supminfxr2  45709  fourierdlem56  46402  ichnreuop  47714