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

Theorem necon2ai 2970
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 139 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2947 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 2941
This theorem is referenced by:  necon2i  2975  intex  5344  iin0  5362  opelopabsb  5535  0ellim  6447  xpord2indlem  8172  ord1eln01  8534  ord2eln012  8535  1ellim  8536  2ellim  8537  0sdom1dom  9274  inf3lem3  9670  cardmin2  10039  pm54.43  10041  pr2ne  10044  canthp1lem2  10693  renepnf  11309  renemnf  11310  lt0ne0d  11828  nnne0ALT  12304  nn0nepnf  12607  hashnemnf  14383  hashnn0n0nn  14430  geolim  15906  geolim2  15907  georeclim  15908  geoisumr  15914  geoisum1c  15916  ramtcl2  17049  lhop1  26053  logdmn0  26682  logcnlem3  26686  bday1s  27876  lrold  27935  mulsval  28135  nbgrssovtx  29378  rusgrnumwwlkl1  29988  strlem1  32269  subfacp1lem1  35184  gonan0  35397  goaln0  35398  rankeq1o  36172  poimirlem9  37636  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem32  37659  pssn0  42266  ensucne0  43542  fouriersw  46246  afvvfveq  47160  fdomne0  48759
  Copyright terms: Public domain W3C validator