Theorem necon2ai 2985

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

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

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 2957

This theorem is used by:  necon2i  2990  intex  5305  iin0  5324  opelopabsb  5504  xpord2indlem  8148  ord1eln01  8488  ord2eln012  8489  1ellim  8490  2ellim  8491  0sdom1dom  9221  inf3lem3  9615  cardmin2  10061  pm54.43  10063  pr2ne  10065  canthp1lem2  10719  renepnf  11338  renemnf  11339  lt0ne0d  11862  nnne0ALT  12357  nn0nepnf  12668  hashnemnf  14468  hashnn0n0nn  14515  geolim  16019  geolim2  16020  georeclim  16021  geoisumr  16027  geoisum1c  16029  ramtcl2  17169  lhop1  26314  logdmn0  26950  logcnlem3  26954  bday1  28182  lrold  28265  mulsval  28477  nbgrssovtx  29924  rusgrnumwwlkl1  30542  strlem1  32834  subfacp1lem1  35913  gonan0  36126  goaln0  36127  rankeq1o  36902  dfttc4lem2  37287  poimirlem9  38515  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem32  38538  pssn0  43249  ensucne0  44488  fouriersw  47185  afvvfveq  48162  fdomne0  49904