Theorem necon2ai 2974

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2944

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 206  df-ne 2945

This theorem is referenced by:  necon2i  2979  intex  5262  iin0  5285  opelopabsb  5444  0ellim  6332  ord1eln01  8335  ord2eln012  8336  1ellim  8337  2ellim  8338  inf3lem3  9397  cardmin2  9766  pm54.43  9768  canthp1lem2  10418  renepnf  11032  renemnf  11033  lt0ne0d  11549  nnne0ALT  12020  nn0nepnf  12322  hashnemnf  14067  hashnn0n0nn  14115  geolim  15591  geolim2  15592  georeclim  15593  geoisumr  15599  geoisum1c  15601  ramtcl2  16721  lhop1  25187  logdmn0  25804  logcnlem3  25808  nbgrssovtx  27737  rusgrnumwwlkl1  28342  strlem1  30621  subfacp1lem1  33150  gonan0  33363  goaln0  33364  xpord2ind  33803  xpord3ind  33809  bday1s  34034  lrold  34086  rankeq1o  34482  poimirlem9  35795  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem32  35818  pssn0  40209  ensucne0  41143  fouriersw  43779  afvvfveq  44651  fdomne0  46188