Theorem necon3ai 2971

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon1ai  2974  necon3i  2979  neneor  3048  nelsn  4688  disjsn2  4737  prnesn  4884  opelopabsb  5549  funsndifnop  7185  ord1eln01  8552  map0b  8941  mapdom3  9215  cflim2  10332  isfin4p1  10384  fpwwe2lem12  10711  tskuni  10852  recextlem2  11921  hashprg  14444  eqsqrt2d  15417  gcd1  16574  gcdzeq  16599  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  phimullem  16826  pcgcd1  16924  pc2dvds  16926  pockthlem  16952  ablfacrplem  20109  znrrg  21607  opnfbas  23871  supfil  23924  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  mpodvdsmulf1o  27255  dvdsmulf1o  27257  ppiub  27266  dchrelbas4  27305  2sqlem8  27488  tgldimor  28528  subfacp1lem6  35153  cvmsss2  35242  ax6e2ndeq  44530  supminfxr2  45384  fourierdlem56  46083  ichnreuop  47346