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

Theorem con2i 122
Description: A contraposition inference. Its associated inference is mt2 181. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
Hypothesis
Ref Expression
con2i.a  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
con2i  |-  ( ps 
->  -.  ph )

Proof of Theorem con2i
StepHypRef Expression
1 con2i.a . 2  |-  ( ph  ->  -.  ps )
2 id 23 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 121 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  nsyl  123  notnot1  124  pm2.65i  175  pm3.14  502  pclem6  933  hba1w  1840  axc4  1886  festino  2351  calemes  2361  fresison  2363  calemos  2364  fesapo  2365  necon3ai  2633  necon2ai  2640  necon2bi  2642  necon4aiOLD  2644  neneqadOLD  2714  eueq3  3226  ssnpss  3548  psstr  3549  elndif  3569  n0i  3745  axnulALT  4525  nfcvb  4623  zfpair  4630  onssneli  5521  onxpdisj  5531  funtpg  5621  ftpg  6063  nlimsucg  6662  reldmtpos  6968  bren2  7586  sdom0  7689  domunsn  7707  sdom1  7757  enp1i  7791  alephval3  8525  dfac2  8545  cdainflem  8605  ackbij1lem18  8651  isfin4-3  8729  fincssdom  8737  fin23lem41  8766  fin45  8806  fin17  8808  fin1a2lem7  8820  axcclem  8871  pwcfsdom  8992  canthp1lem1  9062  hargch  9083  winainflem  9103  ltxrlt  9688  xmullem2  11512  rexmul  11518  xlemul1a  11535  fzdisj  11768  pmtrdifellem4  16830  psgnunilem3  16847  frgpcyg  18912  dvlog2lem  23329  lgsval2lem  23964  isusgra0  24776  usgraop  24779  cusgrares  24901  2pthlem2  25027  2spot0  25493  strlem1  27595  chrelat2i  27710  dfrdg4  30302  finminlem  30559  bj-nimn  30722  hba1-o  31934  hlrelat2  32433  cdleme50ldil  33580  stoweidlem14  37177  alneu  37587  2nodd  38142
  Copyright terms: Public domain W3C validator