Theorem necon2ai 2961

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

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

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 2933

This theorem is referenced by:  necon2i  2966  intex  5289  iin0  5307  opelopabsb  5478  xpord2indlem  8089  ord1eln01  8423  ord2eln012  8424  1ellim  8425  2ellim  8426  0sdom1dom  9146  inf3lem3  9539  cardmin2  9911  pm54.43  9913  pr2ne  9915  canthp1lem2  10564  renepnf  11180  renemnf  11181  lt0ne0d  11702  nnne0ALT  12183  nn0nepnf  12482  hashnemnf  14267  hashnn0n0nn  14314  geolim  15793  geolim2  15794  georeclim  15795  geoisumr  15801  geoisum1c  15803  ramtcl2  16939  lhop1  25975  logdmn0  26605  logcnlem3  26609  bday1  27810  lrold  27893  mulsval  28105  nbgrssovtx  29434  rusgrnumwwlkl1  30044  strlem1  32325  subfacp1lem1  35373  gonan0  35586  goaln0  35587  rankeq1o  36365  poimirlem9  37826  poimirlem18  37835  poimirlem19  37836  poimirlem20  37837  poimirlem32  37849  pssn0  42479  ensucne0  43766  fouriersw  46471  afvvfveq  47390  fdomne0  49091