Theorem necon2ai 3016

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  necon2i  3021  intex  5204  iin0  5226  opelopabsb  5382  0ellim  6221  inf3lem3  9077  cardmin2  9412  pm54.43  9414  canthp1lem2  10064  renepnf  10678  renemnf  10679  lt0ne0d  11194  nnne0ALT  11663  nn0nepnf  11963  hashnemnf  13700  hashnn0n0nn  13748  geolim  15218  geolim2  15219  georeclim  15220  geoisumr  15226  geoisum1c  15228  ramtcl2  16337  lhop1  24617  logdmn0  25231  logcnlem3  25235  nbgrssovtx  27151  rusgrnumwwlkl1  27754  strlem1  30033  subfacp1lem1  32539  gonan0  32752  goaln0  32753  rankeq1o  33745  poimirlem9  35066  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem32  35089  pssn0  39407  ensucne0  40237  fouriersw  42873  afvvfveq  43704