Theorem necon3ai 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon1ai  2960  necon3i  2965  neneor  3033  nelsn  4611  disjsn2  4657  prnesn  4804  opelopabsb  5478  funsndifnop  7098  ord1eln01  8424  map0b  8824  mapdom3  9080  cflim2  10176  isfin4p1  10228  fpwwe2lem12  10556  tskuni  10697  recextlem2  11772  hashprg  14348  eqsqrt2d  15322  gcd1  16488  gcdzeq  16512  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  phimullem  16740  pcgcd1  16839  pc2dvds  16841  pockthlem  16867  ablfacrplem  20033  znrrg  21555  opnfbas  23817  supfil  23870  itg1addlem4  25676  itg1addlem5  25677  mpodvdsmulf1o  27171  dvdsmulf1o  27173  ppiub  27181  dchrelbas4  27220  2sqlem8  27403  tgldimor  28584  subfacp1lem6  35383  cvmsss2  35472  ax6e2ndeq  45004  supminfxr2  45915  fourierdlem56  46608  ichnreuop  47944