MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2i Unicode version

Theorem con2i 115
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
Hypothesis
Ref Expression
con2i.a
Assertion
Ref Expression
con2i

Proof of Theorem con2i
StepHypRef Expression
1 con2i.a . 2
2 id 21 . 2
31, 2nsyl3 114 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  nsyl  116  notnot1  117  pm2.65i  168  pm3.14  492  pclem6  906  hba1w  1745  axc4  1788  sbnOLD  2073  hba1-o  2190  festino  2372  calemes  2382  fresison  2384  calemos  2385  fesapo  2386  necon3ai  2630  necon2bi  2636  necon4ai  2649  neneqad  2660  eueq3  3112  ssnpss  3436  psstr  3437  elndif  3457  n0i  3619  axnulALT  4394  nfcvb  4494  zfpair  4501  onssneli  4799  onxpdisj  4891  funtpg  5438  ftpg  5861  nlimsucg  6423  reldmtpos  6715  bren2  7299  sdom0  7402  domunsn  7420  sdom1  7471  enp1i  7506  alephval3  8227  dfac2  8247  cdainflem  8307  ackbij1lem18  8353  isfin4-3  8431  fincssdom  8439  fin23lem41  8468  fin45  8508  fin17  8510  fin1a2lem7  8522  axcclem  8573  pwcfsdom  8694  canthp1lem1  8765  hargch  8786  winainflem  8806  renfdisj  9383  ltxrlt  9391  xmullem2  11173  rexmul  11179  xlemul1a  11196  fzdisj  11420  pmtrdifellem4  15922  psgnunilem3  15939  frgpcyg  17714  dvlog2lem  21838  lgsval2lem  22386  isusgra0  22954  cusgrares  23059  2pthlem2  23174  strlem1  25333  chrelat2i  25448  dfrdg4  27683  finminlem  28184  stoweidlem14  29483  alneu  29699  2spot0  30331  hlrelat2  32484  cdleme50ldil  33629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator