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

Theorem con2i 114
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 20 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 113 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  nsyl  115  notnot1  116  pm2.65i  167  pm3.14  489  pclem6  897  19.8wOLD  1705  hba1w  1722  ax5o  1765  19.8aOLD  1772  hba1OLD  1805  spimehOLD  1840  spimeOLD  1959  ax12olem3OLD  2013  sbnOLD  2131  spsbeOLD  2147  hba1-o  2226  festino  2386  calemes  2396  fresison  2398  calemos  2399  fesapo  2400  necon3ai  2644  necon2bi  2650  necon4ai  2663  neneqad  2674  eueq3  3109  ssnpss  3450  psstr  3451  elndif  3471  n0i  3633  axnulALT  4336  nfcvb  4394  zfpair  4401  onssneli  4691  nlimsucg  4822  onxpdisj  4957  funtpg  5501  ftpg  5916  reldmtpos  6487  bren2  7138  sdom0  7239  domunsn  7257  sdom1  7308  enp1i  7343  alephval3  7991  dfac2  8011  cdainflem  8071  ackbij1lem18  8117  isfin4-3  8195  fincssdom  8203  fin23lem41  8232  fin45  8272  fin17  8274  fin1a2lem7  8286  axcclem  8337  pwcfsdom  8458  canthp1lem1  8527  hargch  8552  winainflem  8568  renfdisj  9138  ltxrlt  9146  xmullem2  10844  rexmul  10850  xlemul1a  10867  fzdisj  11078  frgpcyg  16854  dvlog2lem  20543  lgsval2lem  21090  isusgra0  21376  cusgrares  21481  2pthlem2  21596  strlem1  23753  chrelat2i  23868  dfrdg4  25795  dvreasin  26290  finminlem  26321  psgnunilem3  27396  stoweidlem14  27739  alneu  27955  2spot0  28453  ax12olem3aAUX7  29457  spimeNEW7  29509  sbnNEW7  29562  spsbeNEW7  29571  hlrelat2  30200  cdleme50ldil  31345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator