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

Theorem necon2ai 2980
 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 2958 1 (𝜑𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2951 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 210  df-ne 2952 This theorem is referenced by:  necon2i  2985  intex  5207  iin0  5229  opelopabsb  5387  0ellim  6231  inf3lem3  9126  cardmin2  9461  pm54.43  9463  canthp1lem2  10113  renepnf  10727  renemnf  10728  lt0ne0d  11243  nnne0ALT  11712  nn0nepnf  12014  hashnemnf  13754  hashnn0n0nn  13802  geolim  15274  geolim2  15275  georeclim  15276  geoisumr  15282  geoisum1c  15284  ramtcl2  16402  lhop1  24713  logdmn0  25330  logcnlem3  25334  nbgrssovtx  27250  rusgrnumwwlkl1  27853  strlem1  30132  subfacp1lem1  32657  gonan0  32870  goaln0  32871  xpord2ind  33349  xpord3ind  33355  bday1s  33607  lrold  33656  rankeq1o  34044  poimirlem9  35368  poimirlem18  35377  poimirlem19  35378  poimirlem20  35379  poimirlem32  35391  pssn0  39729  ensucne0  40632  fouriersw  43261  afvvfveq  44094
 Copyright terms: Public domain W3C validator