Theorem necon3ai 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2932

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 2933

This theorem is referenced by:  necon1ai  2960  necon3i  2965  neneor  3034  nelsn  4660  disjsn2  4708  prnesn  4852  opelopabsb  5520  funsndifnop  7141  ord1eln01  8491  map0b  8873  mapdom3  9145  cflim2  10254  isfin4p1  10306  fpwwe2lem12  10633  tskuni  10774  recextlem2  11842  hashprg  14352  eqsqrt2d  15312  gcd1  16466  gcdzeq  16491  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  phimullem  16711  pcgcd1  16809  pc2dvds  16811  pockthlem  16837  ablfacrplem  19977  znrrg  21428  opnfbas  23668  supfil  23721  itg1addlem4  25550  itg1addlem4OLD  25551  itg1addlem5  25552  mpodvdsmulf1o  27042  dvdsmulf1o  27044  ppiub  27053  dchrelbas4  27092  2sqlem8  27275  tgldimor  28222  subfacp1lem6  34665  cvmsss2  34754  ax6e2ndeq  43809  supminfxr2  44664  fourierdlem56  45363  ichnreuop  46625