Theorem necon3ai 2967

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

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

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 2943

This theorem is referenced by:  necon1ai  2970  necon3i  2975  neneor  3043  nelsn  4598  disjsn2  4645  prnesn  4787  opelopabsb  5436  funsndifnop  7005  map0b  8629  mapdom3  8885  cflim2  9950  isfin4p1  10002  fpwwe2lem12  10329  tskuni  10470  recextlem2  11536  hashprg  14038  eqsqrt2d  15008  gcd1  16163  gcdzeq  16190  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  phimullem  16408  pcgcd1  16506  pc2dvds  16508  pockthlem  16534  ablfacrplem  19583  znrrg  20685  opnfbas  22901  supfil  22954  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  dvdsmulf1o  26248  ppiub  26257  dchrelbas4  26296  2sqlem8  26479  tgldimor  26767  subfacp1lem6  33047  cvmsss2  33136  ax6e2ndeq  42068  supminfxr2  42899  fourierdlem56  43593  ichnreuop  44812