Theorem necon2ai 2985

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon2i  2990  intex  5305  iin0  5324  opelopabsb  5504  xpord2indlem  8165  ord1eln01  8505  ord2eln012  8506  1ellim  8507  2ellim  8508  0sdom1dom  9238  inf3lem3  9632  cardmin2  10081  pm54.43  10083  pr2ne  10085  canthp1lem2  10739  renepnf  11358  renemnf  11359  lt0ne0d  11882  nnne0ALT  12377  nn0nepnf  12688  hashnemnf  14489  hashnn0n0nn  14536  geolim  16040  geolim2  16041  georeclim  16042  geoisumr  16048  geoisum1c  16050  ramtcl2  17190  lhop1  26335  logdmn0  26969  logcnlem3  26973  bday1  28201  lrold  28284  mulsval  28496  nbgrssovtx  29943  rusgrnumwwlkl1  30561  strlem1  32853  subfacp1lem1  35945  gonan0  36158  goaln0  36159  rankeq1o  36933  dfttc4lem2  37318  poimirlem9  38549  poimirlem18  38558  poimirlem19  38559  poimirlem20  38560  poimirlem32  38572  pssn0  43283  ensucne0  44531  fouriersw  47242  afvvfveq  48219  fdomne0  49961