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 1540   ≠ 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  4642  disjsn2  4688  prnesn  4836  opelopabsb  5505  funsndifnop  7141  ord1eln01  8508  map0b  8897  mapdom3  9163  cflim2  10277  isfin4p1  10329  fpwwe2lem12  10656  tskuni  10797  recextlem2  11868  hashprg  14413  eqsqrt2d  15387  gcd1  16547  gcdzeq  16571  lcmfunsnlem2lem1  16657  lcmfunsnlem2lem2  16658  phimullem  16798  pcgcd1  16897  pc2dvds  16899  pockthlem  16925  ablfacrplem  20048  znrrg  21526  opnfbas  23780  supfil  23833  itg1addlem4  25652  itg1addlem5  25653  mpodvdsmulf1o  27156  dvdsmulf1o  27158  ppiub  27167  dchrelbas4  27206  2sqlem8  27389  tgldimor  28481  subfacp1lem6  35207  cvmsss2  35296  ax6e2ndeq  44584  supminfxr2  45496  fourierdlem56  46191  ichnreuop  47486