Theorem necon3ai 2964

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2939

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 2940

This theorem is referenced by:  necon1ai  2967  necon3i  2972  neneor  3041  nelsn  4668  disjsn2  4716  prnesn  4860  opelopabsb  5530  funsndifnop  7151  ord1eln01  8499  map0b  8880  mapdom3  9152  cflim2  10261  isfin4p1  10313  fpwwe2lem12  10640  tskuni  10781  recextlem2  11850  hashprg  14360  eqsqrt2d  15320  gcd1  16474  gcdzeq  16499  lcmfunsnlem2lem1  16580  lcmfunsnlem2lem2  16581  phimullem  16717  pcgcd1  16815  pc2dvds  16817  pockthlem  16843  ablfacrplem  19977  znrrg  21341  opnfbas  23567  supfil  23620  itg1addlem4  25449  itg1addlem4OLD  25450  itg1addlem5  25451  dvdsmulf1o  26935  ppiub  26944  dchrelbas4  26983  2sqlem8  27166  tgldimor  28021  subfacp1lem6  34475  cvmsss2  34564  ax6e2ndeq  43623  supminfxr2  44478  fourierdlem56  45177  ichnreuop  46439