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

Theorem necon2ai 3049
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 3027 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wne 3020
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 3021
This theorem is referenced by:  necon2i  3054  intex  5236  iin0  5257  opelopabsb  5413  0ellim  6250  inf3lem3  9085  cardmin2  9419  pm54.43  9421  canthp1lem2  10067  renepnf  10681  renemnf  10682  lt0ne0d  11197  nnne0ALT  11667  nn0nepnf  11967  hashnemnf  13697  hashnn0n0nn  13745  geolim  15218  geolim2  15219  georeclim  15220  geoisumr  15226  geoisum1c  15228  ramtcl2  16339  lhop1  24528  logdmn0  25138  logcnlem3  25142  nbgrssovtx  27059  rusgrnumwwlkl1  27663  strlem1  29943  subfacp1lem1  32312  gonan0  32525  goaln0  32526  rankeq1o  33518  poimirlem9  34770  poimirlem18  34779  poimirlem19  34780  poimirlem20  34781  poimirlem32  34793  pssn0  38980  ensucne0  39762  fouriersw  42384  afvvfveq  43215
  Copyright terms: Public domain W3C validator