Theorem necon2ai 2957

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

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

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 2929

This theorem is referenced by:  necon2i  2962  intex  5282  iin0  5300  opelopabsb  5470  xpord2indlem  8077  ord1eln01  8411  ord2eln012  8412  1ellim  8413  2ellim  8414  0sdom1dom  9130  inf3lem3  9520  cardmin2  9889  pm54.43  9891  pr2ne  9893  canthp1lem2  10541  renepnf  11157  renemnf  11158  lt0ne0d  11679  nnne0ALT  12160  nn0nepnf  12459  hashnemnf  14248  hashnn0n0nn  14295  geolim  15774  geolim2  15775  georeclim  15776  geoisumr  15782  geoisum1c  15784  ramtcl2  16920  lhop1  25944  logdmn0  26574  logcnlem3  26578  bday1s  27773  lrold  27840  mulsval  28046  nbgrssovtx  29337  rusgrnumwwlkl1  29944  strlem1  32225  subfacp1lem1  35211  gonan0  35424  goaln0  35425  rankeq1o  36204  poimirlem9  37668  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  poimirlem32  37691  pssn0  42259  ensucne0  43561  fouriersw  46268  afvvfveq  47178  fdomne0  48880