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, 5-Aug-1993.) (Proof shortened by 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  499  pclem6  916  hba1w  1757  axc4  1800  sbnOLD  2088  hba1-o  2203  festino  2391  calemes  2401  fresison  2403  calemos  2404  fesapo  2405  necon3ai  2649  necon2bi  2655  necon4ai  2668  neneqad  2679  eueq3  3131  ssnpss  3456  psstr  3457  elndif  3477  n0i  3639  axnulALT  4416  nfcvb  4519  zfpair  4526  onssneli  4824  onxpdisj  4916  funtpg  5465  ftpg  5889  nlimsucg  6452  reldmtpos  6752  bren2  7336  sdom0  7439  domunsn  7457  sdom1  7508  enp1i  7543  alephval3  8276  dfac2  8296  cdainflem  8356  ackbij1lem18  8402  isfin4-3  8480  fincssdom  8488  fin23lem41  8517  fin45  8557  fin17  8559  fin1a2lem7  8571  axcclem  8622  pwcfsdom  8743  canthp1lem1  8815  hargch  8836  winainflem  8856  renfdisj  9433  ltxrlt  9441  xmullem2  11224  rexmul  11230  xlemul1a  11247  fzdisj  11472  pmtrdifellem4  15978  psgnunilem3  15995  frgpcyg  17965  dvlog2lem  22056  lgsval2lem  22604  isusgra0  23210  cusgrares  23315  2pthlem2  23430  strlem1  25589  chrelat2i  25704  dfrdg4  27910  finminlem  28438  stoweidlem14  29734  alneu  29950  2spot0  30582  hlrelat2  32769  cdleme50ldil  33914
  Copyright terms: Public domain W3C validator