Theorem necon2ai 2968

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

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

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 2939

This theorem is referenced by:  necon2i  2973  intex  5350  iin0  5368  opelopabsb  5540  0ellim  6449  xpord2indlem  8171  ord1eln01  8533  ord2eln012  8534  1ellim  8535  2ellim  8536  0sdom1dom  9272  inf3lem3  9668  cardmin2  10037  pm54.43  10039  pr2ne  10042  canthp1lem2  10691  renepnf  11307  renemnf  11308  lt0ne0d  11826  nnne0ALT  12302  nn0nepnf  12605  hashnemnf  14380  hashnn0n0nn  14427  geolim  15903  geolim2  15904  georeclim  15905  geoisumr  15911  geoisum1c  15913  ramtcl2  17045  lhop1  26068  logdmn0  26697  logcnlem3  26701  bday1s  27891  lrold  27950  mulsval  28150  nbgrssovtx  29393  rusgrnumwwlkl1  29998  strlem1  32279  subfacp1lem1  35164  gonan0  35377  goaln0  35378  rankeq1o  36153  poimirlem9  37616  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem32  37639  pssn0  42245  ensucne0  43519  fouriersw  46187  afvvfveq  47098  fdomne0  48680