Theorem necon2ai 2988

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

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

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 2960

This theorem is used by:  necon2i  2993  intex  5310  iin0  5329  opelopabsb  5509  xpord2indlem  8194  ord1eln01  8535  ord2eln012  8536  1ellim  8537  2ellim  8538  0sdom1dom  9268  inf3lem3  9661  cardmin2  10110  pm54.43  10112  pr2ne  10114  canthp1lem2  10768  renepnf  11387  renemnf  11388  lt0ne0d  11911  nnne0ALT  12406  nn0nepnf  12717  hashnemnf  14518  hashnn0n0nn  14565  geolim  16071  geolim2  16072  georeclim  16073  geoisumr  16079  geoisum1c  16081  ramtcl2  17221  lhop1  26367  logdmn0  27001  logcnlem3  27005  bday1  28233  lrold  28316  mulsval  28528  nbgrssovtx  29975  rusgrnumwwlkl1  30593  strlem1  32885  subfacp1lem1  36124  gonan0  36337  goaln0  36338  rankeq1o  37123  dfttc4lem2  37508  poimirlem9  38752  poimirlem18  38761  poimirlem19  38762  poimirlem20  38763  poimirlem32  38775  pssn0  43485  ensucne0  44733  fouriersw  47456  afvvfveq  48433  fdomne0  50176