Theorem necon3ai 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  necon1ai  2952  necon3i  2957  neneor  3025  nelsn  4630  disjsn2  4676  prnesn  4824  opelopabsb  5490  funsndifnop  7123  ord1eln01  8460  map0b  8856  mapdom3  9113  cflim2  10216  isfin4p1  10268  fpwwe2lem12  10595  tskuni  10736  recextlem2  11809  hashprg  14360  eqsqrt2d  15335  gcd1  16498  gcdzeq  16522  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  phimullem  16749  pcgcd1  16848  pc2dvds  16850  pockthlem  16876  ablfacrplem  19997  znrrg  21475  opnfbas  23729  supfil  23782  itg1addlem4  25600  itg1addlem5  25601  mpodvdsmulf1o  27104  dvdsmulf1o  27106  ppiub  27115  dchrelbas4  27154  2sqlem8  27337  tgldimor  28429  subfacp1lem6  35172  cvmsss2  35261  ax6e2ndeq  44549  supminfxr2  45465  fourierdlem56  46160  ichnreuop  47473