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  928  hba1w  1763  axc4  1809  sbnOLD  2106  hba1-o  2221  festino  2414  calemes  2424  fresison  2426  calemos  2427  fesapo  2428  necon3ai  2695  necon2ai  2702  necon2bi  2704  necon4aiOLD  2706  neneqadOLD  2776  eueq3  3278  ssnpss  3607  psstr  3608  elndif  3628  n0i  3790  axnulALT  4574  nfcvb  4677  zfpair  4684  onssneli  4987  onxpdisj  5081  funtpg  5636  ftpg  6069  nlimsucg  6655  reldmtpos  6960  bren2  7543  sdom0  7646  domunsn  7664  sdom1  7716  enp1i  7751  alephval3  8487  dfac2  8507  cdainflem  8567  ackbij1lem18  8613  isfin4-3  8691  fincssdom  8699  fin23lem41  8728  fin45  8768  fin17  8770  fin1a2lem7  8782  axcclem  8833  pwcfsdom  8954  canthp1lem1  9026  hargch  9047  winainflem  9067  renfdisj  9643  ltxrlt  9651  xmullem2  11453  rexmul  11459  xlemul1a  11476  fzdisj  11708  pmtrdifellem4  16300  psgnunilem3  16317  frgpcyg  18379  dvlog2lem  22761  lgsval2lem  23309  isusgra0  24023  usgraop  24026  cusgrares  24148  2pthlem2  24274  2spot0  24741  strlem1  26845  chrelat2i  26960  dfrdg4  29177  finminlem  29713  stoweidlem14  31314  fourierswlem  31531  fouriersw  31532  alneu  31673  hlrelat2  34199  cdleme50ldil  35344
  Copyright terms: Public domain W3C validator