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

Theorem con2i 120
Description: A contraposition inference. (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 22 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 119 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  121  notnot1  122  pm2.65i  173  pm3.14  502  pclem6  921  hba1w  1752  axc4  1795  sbnOLD  2083  hba1-o  2199  festino  2392  calemes  2402  fresison  2404  calemos  2405  fesapo  2406  necon3ai  2666  necon2bi  2672  necon4ai  2685  neneqad  2696  eueq3  3149  ssnpss  3474  psstr  3475  elndif  3495  n0i  3657  axnulALT  4434  nfcvb  4537  zfpair  4544  onssneli  4843  onxpdisj  4935  funtpg  5483  ftpg  5907  nlimsucg  6468  reldmtpos  6768  bren2  7355  sdom0  7458  domunsn  7476  sdom1  7527  enp1i  7562  alephval3  8295  dfac2  8315  cdainflem  8375  ackbij1lem18  8421  isfin4-3  8499  fincssdom  8507  fin23lem41  8536  fin45  8576  fin17  8578  fin1a2lem7  8590  axcclem  8641  pwcfsdom  8762  canthp1lem1  8834  hargch  8855  winainflem  8875  renfdisj  9452  ltxrlt  9460  xmullem2  11243  rexmul  11249  xlemul1a  11266  fzdisj  11491  pmtrdifellem4  16000  psgnunilem3  16017  frgpcyg  18021  dvlog2lem  22112  lgsval2lem  22660  isusgra0  23290  cusgrares  23395  2pthlem2  23510  strlem1  25669  chrelat2i  25784  dfrdg4  27996  finminlem  28532  stoweidlem14  29828  alneu  30044  2spot0  30676  hlrelat2  33066  cdleme50ldil  34211
  Copyright terms: Public domain W3C validator