Theorem necon3ai 2958

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

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

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 2934

This theorem is referenced by:  necon1ai  2960  necon3i  2965  neneor  3033  nelsn  4625  disjsn2  4671  prnesn  4818  opelopabsb  5486  funsndifnop  7106  ord1eln01  8433  map0b  8833  mapdom3  9089  cflim2  10185  isfin4p1  10237  fpwwe2lem12  10565  tskuni  10706  recextlem2  11780  hashprg  14330  eqsqrt2d  15304  gcd1  16467  gcdzeq  16491  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  phimullem  16718  pcgcd1  16817  pc2dvds  16819  pockthlem  16845  ablfacrplem  20008  znrrg  21532  opnfbas  23798  supfil  23851  itg1addlem4  25668  itg1addlem5  25669  mpodvdsmulf1o  27172  dvdsmulf1o  27174  ppiub  27183  dchrelbas4  27222  2sqlem8  27405  tgldimor  28586  subfacp1lem6  35398  cvmsss2  35487  ax6e2ndeq  44909  supminfxr2  45821  fourierdlem56  46514  ichnreuop  47826