Theorem necon2ai 2990

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

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

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 2962

This theorem is used by:  necon2i  2995  intex  5319  iin0  5338  opelopabsb  5519  xpord2indlem  8152  ord1eln01  8490  ord2eln012  8491  1ellim  8492  2ellim  8493  0sdom1dom  9216  inf3lem3  9609  cardmin2  10004  pm54.43  10006  pr2ne  10008  canthp1lem2  10656  renepnf  11275  renemnf  11276  lt0ne0d  11797  nnne0ALT  12292  nn0nepnf  12603  hashnemnf  14400  hashnn0n0nn  14447  geolim  15950  geolim2  15951  georeclim  15952  geoisumr  15958  geoisum1c  15960  ramtcl2  17096  lhop1  26210  logdmn0  26842  logcnlem3  26846  bday1  28044  lrold  28127  mulsval  28339  nbgrssovtx  29748  rusgrnumwwlkl1  30357  strlem1  32639  subfacp1lem1  35692  gonan0  35905  goaln0  35906  rankeq1o  36684  dfttc4lem2  37081  poimirlem9  38321  poimirlem18  38330  poimirlem19  38331  poimirlem20  38332  poimirlem32  38344  pssn0  43039  ensucne0  44296  fouriersw  46986  afvvfveq  47926  fdomne0  49669