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

Theorem necon2ai 2925
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 134 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2903 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1596  wne 2896
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 197  df-ne 2897
This theorem is referenced by:  necon2i  2930  intex  4925  iin0  4944  opelopabsb  5089  0ellim  5900  inf3lem3  8640  cardmin2  8937  pm54.43  8939  canthp1lem2  9588  renepnf  10200  renemnf  10201  lt0ne0d  10706  nnne0  11166  nn0nepnf  11484  hashnemnf  13247  hashnn0n0nn  13293  geolim  14721  geolim2  14722  georeclim  14723  geoisumr  14729  geoisum1c  14731  ramtcl2  15838  lhop1  23897  logdmn0  24506  logcnlem3  24510  nbgrssovtx  26377  rusgrnumwwlkl1  27011  strlem1  29339  subfacp1lem1  31389  rankeq1o  32505  poimirlem9  33650  poimirlem18  33659  poimirlem19  33660  poimirlem20  33661  poimirlem32  33673  fouriersw  40868  afvvfveq  41651
  Copyright terms: Public domain W3C validator