Theorem necon3ai 2983

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  necon1ai  2985  necon3i  2990  neneor  3060  nelsn  4633  disjsn2  4679  prnesn  4826  opelopabsb  5516  funsndifnop  7150  ord1eln01  8482  map0b  8882  mapdom3  9138  cflim2  10248  isfin4p1  10300  fpwwe2lem12  10628  tskuni  10769  recextlem2  11846  hashprg  14433  eqsqrt2d  15422  gcd1  16587  gcdzeq  16611  lcmfunsnlem2lem1  16697  lcmfunsnlem2lem2  16698  phimullem  16839  pcgcd1  16938  pc2dvds  16940  pockthlem  16966  ablfacrplem  20138  znrrg  21696  opnfbas  23980  supfil  24033  itg1addlem4  25839  itg1addlem5  25840  mpodvdsmulf1o  27339  dvdsmulf1o  27341  ppiub  27349  dchrelbas4  27388  2sqlem8  27571  tgldimor  28752  subfacp1lem6  35658  cvmsss2  35747  ax6e2ndeq  45251  supminfxr2  46166  fourierdlem56  46859  ichnreuop  48204