MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2i 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 21 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 113 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  nsyl  115  notnot1  116  pm2.65i  167  pm3.14  490  pclem6  898  19.8w  1660  hba1w  1682  ax5o  1718  19.8a  1719  hba1  1720  spimeh  1723  ax12olem3  1871  spime  1918  sbn  2001  spsbe  2014  hba1-o  2090  festino  2249  calemes  2259  fresison  2261  calemos  2262  fesapo  2263  necon3ai  2487  necon2bi  2493  necon4ai  2506  neneqad  2517  eueq3  2941  ssnpss  3280  psstr  3281  elndif  3301  n0i  3461  nfcvb  4204  zfpair  4211  onssneli  4501  nlimsucg  4632  onxpdisj  4768  reldmtpos  6203  bren2  6887  sdom0  6988  domunsn  7006  sdom1  7057  enp1i  7088  alephval3  7732  dfac2  7752  cdainflem  7812  ackbij1lem18  7858  isfin4-3  7936  fincssdom  7944  fin23lem41  7973  fin45  8013  fin17  8015  fin1a2lem7  8027  axcclem  8078  pwcfsdom  8200  canthp1lem1  8269  hargch  8294  winainflem  8310  renfdisj  8880  ltxrlt  8888  xmullem2  10579  rexmul  10585  xlemul1a  10602  fzdisj  10811  frgpcyg  16521  dvlog2lem  19993  lgsval2lem  20539  strlem1  22822  chrelat2i  22937  axfelem18  23764  axfelem22  23768  dfrdg4  23895  finminlem  25630  psgnunilem3  26818  stoweidlem14  27162  ax12-4  28373  ax12conj2  28375  a12study8  28386  a12study  28399  ax9lem7  28413  ax9lem12  28418  ax9lem15  28421  hlrelat2  28859  cdleme50ldil  30004
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator