Theorem necon2ai 2986

Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon2ai.1	⊢ (𝐴 = 𝐵 → ¬ 𝜑)

Assertion

Ref	Expression
necon2ai	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem necon2ai

Step	Hyp	Ref	Expression
1		necon2ai.1	. . 3 ⊢ (𝐴 = 𝐵 → ¬ 𝜑)
2	1	con2i 140	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2964	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  necon2i  2991  intex  5312  iin0  5331  opelopabsb  5512  xpord2indlem  8149  ord1eln01  8487  ord2eln012  8488  1ellim  8489  2ellim  8490  0sdom1dom  9220  inf3lem3  9613  cardmin2  10008  pm54.43  10010  pr2ne  10012  canthp1lem2  10666  renepnf  11285  renemnf  11286  lt0ne0d  11807  nnne0ALT  12302  nn0nepnf  12613  hashnemnf  14412  hashnn0n0nn  14459  geolim  15963  geolim2  15964  georeclim  15965  geoisumr  15971  geoisum1c  15973  ramtcl2  17109  lhop1  26248  logdmn0  26885  logcnlem3  26889  bday1  28087  lrold  28170  mulsval  28382  nbgrssovtx  29829  rusgrnumwwlkl1  30447  strlem1  32739  subfacp1lem1  35766  gonan0  35979  goaln0  35980  rankeq1o  36759  dfttc4lem2  37156  poimirlem9  38386  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem32  38409  pssn0  43105  ensucne0  44377  fouriersw  47067  afvvfveq  48044  fdomne0  49786