Theorem necon2ai 2987

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  necon2i  2992  intex  5316  iin0  5335  opelopabsb  5516  xpord2indlem  8144  ord1eln01  8482  ord2eln012  8483  1ellim  8484  2ellim  8485  0sdom1dom  9207  inf3lem3  9600  cardmin2  9986  pm54.43  9988  pr2ne  9990  canthp1lem2  10639  renepnf  11258  renemnf  11259  lt0ne0d  11780  nnne0ALT  12275  nn0nepnf  12586  hashnemnf  14382  hashnn0n0nn  14429  geolim  15926  geolim2  15927  georeclim  15928  geoisumr  15934  geoisum1c  15936  ramtcl2  17072  lhop1  26154  logdmn0  26786  logcnlem3  26790  bday1  27988  lrold  28071  mulsval  28283  nbgrssovtx  29692  rusgrnumwwlkl1  30301  strlem1  32583  subfacp1lem1  35652  gonan0  35865  goaln0  35866  rankeq1o  36644  dfttc4lem2  37021  poimirlem9  38261  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem32  38284  pssn0  42979  ensucne0  44238  fouriersw  46928  afvvfveq  47868  fdomne0  49611