Theorem necon2ai 2970

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 139	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2947	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  necon2i  2975  intex  5337  iin0  5360  opelopabsb  5530  0ellim  6427  xpord2indlem  8135  ord1eln01  8498  ord2eln012  8499  1ellim  8500  2ellim  8501  0sdom1dom  9240  inf3lem3  9627  cardmin2  9996  pm54.43  9998  pr2ne  10001  canthp1lem2  10650  renepnf  11264  renemnf  11265  lt0ne0d  11781  nnne0ALT  12252  nn0nepnf  12554  hashnemnf  14306  hashnn0n0nn  14353  geolim  15818  geolim2  15819  georeclim  15820  geoisumr  15826  geoisum1c  15828  ramtcl2  16946  lhop1  25538  logdmn0  26155  logcnlem3  26159  bday1s  27340  lrold  27399  mulsval  27575  nbgrssovtx  28656  rusgrnumwwlkl1  29260  strlem1  31541  subfacp1lem1  34239  gonan0  34452  goaln0  34453  rankeq1o  35212  poimirlem9  36583  poimirlem18  36592  poimirlem19  36593  poimirlem20  36594  poimirlem32  36606  pssn0  41131  ensucne0  42362  fouriersw  45026  afvvfveq  45935  fdomne0  47594