Theorem necon3ai 2964

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

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

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 2940

This theorem is referenced by:  necon1ai  2967  necon3i  2972  neneor  3041  nelsn  4631  disjsn2  4678  prnesn  4822  opelopabsb  5492  funsndifnop  7102  ord1eln01  8447  map0b  8828  mapdom3  9100  cflim2  10208  isfin4p1  10260  fpwwe2lem12  10587  tskuni  10728  recextlem2  11795  hashprg  14305  eqsqrt2d  15265  gcd1  16419  gcdzeq  16444  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  phimullem  16662  pcgcd1  16760  pc2dvds  16762  pockthlem  16788  ablfacrplem  19858  znrrg  21009  opnfbas  23230  supfil  23283  itg1addlem4  25100  itg1addlem4OLD  25101  itg1addlem5  25102  dvdsmulf1o  26580  ppiub  26589  dchrelbas4  26628  2sqlem8  26811  tgldimor  27507  subfacp1lem6  33866  cvmsss2  33955  ax6e2ndeq  42963  supminfxr2  43824  fourierdlem56  44523  ichnreuop  45784