Theorem necon3ai 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  necon1ai  2965  necon3i  2970  neneor  3039  nelsn  4670  disjsn2  4716  prnesn  4864  opelopabsb  5539  funsndifnop  7170  ord1eln01  8532  map0b  8921  mapdom3  9187  cflim2  10300  isfin4p1  10352  fpwwe2lem12  10679  tskuni  10820  recextlem2  11891  hashprg  14430  eqsqrt2d  15403  gcd1  16561  gcdzeq  16585  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  phimullem  16812  pcgcd1  16910  pc2dvds  16912  pockthlem  16938  ablfacrplem  20099  znrrg  21601  opnfbas  23865  supfil  23918  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  mpodvdsmulf1o  27251  dvdsmulf1o  27253  ppiub  27262  dchrelbas4  27301  2sqlem8  27484  tgldimor  28524  subfacp1lem6  35169  cvmsss2  35258  ax6e2ndeq  44556  supminfxr2  45418  fourierdlem56  46117  ichnreuop  47396