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

Theorem con2i 125
Description: A contraposition inference. Its associated inference is mt2 184. (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 124 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  126  notnot1  127  pm2.65i  178  pm3.14  509  pclem6  946  hba1w  1894  axc4  1949  festino  2411  calemes  2421  fresison  2423  calemos  2424  fesapo  2425  necon3ai  2661  necon2ai  2665  necon2bi  2666  eueq3  3225  ssnpss  3548  psstr  3549  elndif  3569  n0i  3748  axnulALT  4547  nfcvb  4647  zfpair  4654  onssneli  5555  onxpdisj  5565  funtpg  5655  ftpg  6103  nlimsucg  6701  reldmtpos  7012  bren2  7631  sdom0  7735  domunsn  7753  sdom1  7803  enp1i  7837  alephval3  8572  dfac2  8592  cdainflem  8652  ackbij1lem18  8698  isfin4-3  8776  fincssdom  8784  fin23lem41  8813  fin45  8853  fin17  8855  fin1a2lem7  8867  axcclem  8918  pwcfsdom  9039  canthp1lem1  9108  hargch  9129  winainflem  9149  ltxrlt  9735  xmullem2  11585  rexmul  11591  xlemul1a  11608  fzdisj  11861  lcmfunsnlem2lem2  14667  pmtrdifellem4  17175  psgnunilem3  17192  frgpcyg  19199  dvlog2lem  23653  lgsval2lem  24290  isusgra0  25130  usgraop  25133  cusgrares  25256  2pthlem2  25382  2spot0  25848  strlem1  27959  chrelat2i  28074  dfrdg4  30768  finminlem  31024  bj-nimn  31184  finxpreclem3  31831  finxpreclem5  31833  hba1-o  32515  hlrelat2  33014  cdleme50ldil  34161  stoweidlem14  37975  alneu  38757  2nodd  40181
  Copyright terms: Public domain W3C validator