Theorem necon3ai 2957

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

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

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 2933

This theorem is referenced by:  necon1ai  2959  necon3i  2964  neneor  3032  nelsn  4610  disjsn2  4656  prnesn  4803  opelopabsb  5485  funsndifnop  7105  ord1eln01  8431  map0b  8831  mapdom3  9087  cflim2  10185  isfin4p1  10237  fpwwe2lem12  10565  tskuni  10706  recextlem2  11781  hashprg  14357  eqsqrt2d  15331  gcd1  16497  gcdzeq  16521  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  phimullem  16749  pcgcd1  16848  pc2dvds  16850  pockthlem  16876  ablfacrplem  20042  znrrg  21545  opnfbas  23807  supfil  23860  itg1addlem4  25666  itg1addlem5  25667  mpodvdsmulf1o  27157  dvdsmulf1o  27159  ppiub  27167  dchrelbas4  27206  2sqlem8  27389  tgldimor  28570  subfacp1lem6  35367  cvmsss2  35456  ax6e2ndeq  44986  supminfxr2  45897  fourierdlem56  46590  ichnreuop  47932