Theorem necon2ai 2972

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

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

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 2943

This theorem is referenced by:  necon2i  2977  intex  5256  iin0  5279  opelopabsb  5436  0ellim  6313  inf3lem3  9318  cardmin2  9688  pm54.43  9690  canthp1lem2  10340  renepnf  10954  renemnf  10955  lt0ne0d  11470  nnne0ALT  11941  nn0nepnf  12243  hashnemnf  13986  hashnn0n0nn  14034  geolim  15510  geolim2  15511  georeclim  15512  geoisumr  15518  geoisum1c  15520  ramtcl2  16640  lhop1  25083  logdmn0  25700  logcnlem3  25704  nbgrssovtx  27631  rusgrnumwwlkl1  28234  strlem1  30513  subfacp1lem1  33041  gonan0  33254  goaln0  33255  xpord2ind  33721  xpord3ind  33727  bday1s  33952  lrold  34004  rankeq1o  34400  poimirlem9  35713  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem32  35736  pssn0  40128  ensucne0  41034  fouriersw  43662  afvvfveq  44527  fdomne0  46065