Theorem necon3ai 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon1ai  2956  necon3i  2961  neneor  3029  nelsn  4618  disjsn2  4664  prnesn  4811  opelopabsb  5473  funsndifnop  7090  ord1eln01  8417  map0b  8813  mapdom3  9069  cflim2  10161  isfin4p1  10213  fpwwe2lem12  10540  tskuni  10681  recextlem2  11755  hashprg  14304  eqsqrt2d  15278  gcd1  16441  gcdzeq  16465  lcmfunsnlem2lem1  16551  lcmfunsnlem2lem2  16552  phimullem  16692  pcgcd1  16791  pc2dvds  16793  pockthlem  16819  ablfacrplem  19981  znrrg  21504  opnfbas  23758  supfil  23811  itg1addlem4  25628  itg1addlem5  25629  mpodvdsmulf1o  27132  dvdsmulf1o  27134  ppiub  27143  dchrelbas4  27182  2sqlem8  27365  tgldimor  28481  subfacp1lem6  35250  cvmsss2  35339  ax6e2ndeq  44676  supminfxr2  45591  fourierdlem56  46284  ichnreuop  47596