Theorem necon2ai 2980

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

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

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 2952

This theorem is referenced by:  necon2i  2985  intex  5207  iin0  5229  opelopabsb  5387  0ellim  6231  inf3lem3  9126  cardmin2  9461  pm54.43  9463  canthp1lem2  10113  renepnf  10727  renemnf  10728  lt0ne0d  11243  nnne0ALT  11712  nn0nepnf  12014  hashnemnf  13754  hashnn0n0nn  13802  geolim  15274  geolim2  15275  georeclim  15276  geoisumr  15282  geoisum1c  15284  ramtcl2  16402  lhop1  24713  logdmn0  25330  logcnlem3  25334  nbgrssovtx  27250  rusgrnumwwlkl1  27853  strlem1  30132  subfacp1lem1  32657  gonan0  32870  goaln0  32871  xpord2ind  33349  xpord3ind  33355  bday1s  33607  lrold  33656  rankeq1o  34044  poimirlem9  35368  poimirlem18  35377  poimirlem19  35378  poimirlem20  35379  poimirlem32  35391  pssn0  39729  ensucne0  40632  fouriersw  43261  afvvfveq  44094