MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2ai Structured version   Visualization version   GIF version

Theorem necon2ai 3045
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
StepHypRef Expression
1 necon2ai.1 . . 3 (𝐴 = 𝐵 → ¬ 𝜑)
21con2i 141 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32neqned 3023 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon2i  3050  intex  5232  iin0  5253  opelopabsb  5409  0ellim  6247  inf3lem3  9082  cardmin2  9416  pm54.43  9418  canthp1lem2  10064  renepnf  10678  renemnf  10679  lt0ne0d  11194  nnne0ALT  11664  nn0nepnf  11964  hashnemnf  13694  hashnn0n0nn  13742  geolim  15216  geolim2  15217  georeclim  15218  geoisumr  15224  geoisum1c  15226  ramtcl2  16337  lhop1  24540  logdmn0  25150  logcnlem3  25154  nbgrssovtx  27071  rusgrnumwwlkl1  27675  strlem1  29955  subfacp1lem1  32324  gonan0  32537  goaln0  32538  rankeq1o  33530  poimirlem9  34783  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem32  34806  pssn0  38993  ensucne0  39775  fouriersw  42397  afvvfveq  43228
  Copyright terms: Public domain W3C validator