Theorem necon2ai 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  necon2i  2959  intex  5299  iin0  5317  opelopabsb  5490  xpord2indlem  8126  ord1eln01  8460  ord2eln012  8461  1ellim  8462  2ellim  8463  0sdom1dom  9185  inf3lem3  9583  cardmin2  9952  pm54.43  9954  pr2ne  9957  canthp1lem2  10606  renepnf  11222  renemnf  11223  lt0ne0d  11743  nnne0ALT  12224  nn0nepnf  12523  hashnemnf  14309  hashnn0n0nn  14356  geolim  15836  geolim2  15837  georeclim  15838  geoisumr  15844  geoisum1c  15846  ramtcl2  16982  lhop1  25919  logdmn0  26549  logcnlem3  26553  bday1s  27743  lrold  27808  mulsval  28012  nbgrssovtx  29288  rusgrnumwwlkl1  29898  strlem1  32179  subfacp1lem1  35166  gonan0  35379  goaln0  35380  rankeq1o  36159  poimirlem9  37623  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem32  37646  pssn0  42215  ensucne0  43518  fouriersw  46229  afvvfveq  47149  fdomne0  48838