Theorem necon3ai 2966

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necon1ai  2969  necon3i  2974  neneor  3043  nelsn  4669  disjsn2  4717  prnesn  4861  opelopabsb  5531  funsndifnop  7149  ord1eln01  8496  map0b  8877  mapdom3  9149  cflim2  10258  isfin4p1  10310  fpwwe2lem12  10637  tskuni  10778  recextlem2  11845  hashprg  14355  eqsqrt2d  15315  gcd1  16469  gcdzeq  16494  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  phimullem  16712  pcgcd1  16810  pc2dvds  16812  pockthlem  16838  ablfacrplem  19935  znrrg  21121  opnfbas  23346  supfil  23399  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  dvdsmulf1o  26698  ppiub  26707  dchrelbas4  26746  2sqlem8  26929  tgldimor  27753  subfacp1lem6  34176  cvmsss2  34265  ax6e2ndeq  43320  supminfxr2  44179  fourierdlem56  44878  ichnreuop  46140