Theorem necon3ai 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon1ai  2952  necon3i  2957  neneor  3025  nelsn  4620  disjsn2  4666  prnesn  4814  opelopabsb  5477  funsndifnop  7089  ord1eln01  8421  map0b  8817  mapdom3  9073  cflim2  10176  isfin4p1  10228  fpwwe2lem12  10555  tskuni  10696  recextlem2  11769  hashprg  14320  eqsqrt2d  15294  gcd1  16457  gcdzeq  16481  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  phimullem  16708  pcgcd1  16807  pc2dvds  16809  pockthlem  16835  ablfacrplem  19964  znrrg  21490  opnfbas  23745  supfil  23798  itg1addlem4  25616  itg1addlem5  25617  mpodvdsmulf1o  27120  dvdsmulf1o  27122  ppiub  27131  dchrelbas4  27170  2sqlem8  27353  tgldimor  28465  subfacp1lem6  35157  cvmsss2  35246  ax6e2ndeq  44533  supminfxr2  45449  fourierdlem56  46144  ichnreuop  47457