Theorem necon3ai 2960

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon1ai  2962  necon3i  2967  neneor  3035  nelsn  4605  disjsn2  4651  prnesn  4798  opelopabsb  5479  funsndifnop  7101  ord1eln01  8428  map0b  8828  mapdom3  9084  cflim2  10183  isfin4p1  10235  fpwwe2lem12  10563  tskuni  10704  recextlem2  11779  hashprg  14355  eqsqrt2d  15329  gcd1  16495  gcdzeq  16519  lcmfunsnlem2lem1  16605  lcmfunsnlem2lem2  16606  phimullem  16747  pcgcd1  16846  pc2dvds  16848  pockthlem  16874  ablfacrplem  20040  znrrg  21547  opnfbas  23832  supfil  23885  itg1addlem4  25691  itg1addlem5  25692  mpodvdsmulf1o  27182  dvdsmulf1o  27184  ppiub  27192  dchrelbas4  27231  2sqlem8  27414  tgldimor  28595  subfacp1lem6  35420  cvmsss2  35509  ax6e2ndeq  45010  supminfxr2  45919  fourierdlem56  46612  ichnreuop  47954