Theorem necon3ai 2963

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

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

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 2939

This theorem is referenced by:  necon1ai  2966  necon3i  2971  neneor  3040  nelsn  4667  disjsn2  4715  prnesn  4859  opelopabsb  5529  funsndifnop  7150  ord1eln01  8498  map0b  8879  mapdom3  9151  cflim2  10260  isfin4p1  10312  fpwwe2lem12  10639  tskuni  10780  recextlem2  11849  hashprg  14359  eqsqrt2d  15319  gcd1  16473  gcdzeq  16498  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  phimullem  16716  pcgcd1  16814  pc2dvds  16816  pockthlem  16842  ablfacrplem  19976  znrrg  21340  opnfbas  23566  supfil  23619  itg1addlem4  25448  itg1addlem4OLD  25449  itg1addlem5  25450  dvdsmulf1o  26934  ppiub  26943  dchrelbas4  26982  2sqlem8  27165  tgldimor  28020  subfacp1lem6  34474  cvmsss2  34563  ax6e2ndeq  43622  supminfxr2  44477  fourierdlem56  45176  ichnreuop  46438