Theorem necon3ai 2985

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  necon1ai  2987  necon3i  2992  neneor  3060  nelsn  4628  disjsn2  4674  prnesn  4821  opelopabsb  5505  funsndifnop  7138  ord1eln01  8469  map0b  8869  mapdom3  9125  cflim2  10235  isfin4p1  10287  fpwwe2lem12  10615  tskuni  10756  recextlem2  11833  hashprg  14422  eqsqrt2d  15410  gcd1  16576  gcdzeq  16600  lcmfunsnlem2lem1  16686  lcmfunsnlem2lem2  16687  phimullem  16828  pcgcd1  16927  pc2dvds  16929  pockthlem  16955  ablfacrplem  20128  znrrg  21675  opnfbas  23960  supfil  24013  itg1addlem4  25819  itg1addlem5  25820  mpodvdsmulf1o  27316  dvdsmulf1o  27318  ppiub  27326  dchrelbas4  27365  2sqlem8  27548  tgldimor  28729  subfacp1lem6  35548  cvmsss2  35637  ax6e2ndeq  45133  supminfxr2  46041  fourierdlem56  46734  ichnreuop  48076