Theorem necon2ai 2976

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 2953	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon2i  2981  intex  5362  iin0  5380  opelopabsb  5549  0ellim  6458  xpord2indlem  8188  ord1eln01  8552  ord2eln012  8553  1ellim  8554  2ellim  8555  0sdom1dom  9301  inf3lem3  9699  cardmin2  10068  pm54.43  10070  pr2ne  10073  canthp1lem2  10722  renepnf  11338  renemnf  11339  lt0ne0d  11855  nnne0ALT  12331  nn0nepnf  12633  hashnemnf  14393  hashnn0n0nn  14440  geolim  15918  geolim2  15919  georeclim  15920  geoisumr  15926  geoisum1c  15928  ramtcl2  17058  lhop1  26073  logdmn0  26700  logcnlem3  26704  bday1s  27894  lrold  27953  mulsval  28153  nbgrssovtx  29396  rusgrnumwwlkl1  30001  strlem1  32282  subfacp1lem1  35147  gonan0  35360  goaln0  35361  rankeq1o  36135  poimirlem9  37589  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem32  37612  pssn0  42220  ensucne0  43491  fouriersw  46152  afvvfveq  47063  fdomne0  48563