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

Theorem con2i 112
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 19 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 111 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  nsyl  113  notnot1  114  pm2.65i  165  pm3.14  488  pclem6  896  19.8w  1659  hba1w  1681  ax5o  1717  19.8a  1718  hba1  1719  spimeh  1722  ax12olem3  1870  spime  1916  sbn  2002  spsbe  2015  hba1-o  2088  festino  2248  calemes  2258  fresison  2260  calemos  2261  fesapo  2262  necon3ai  2486  necon2bi  2492  necon4ai  2505  neneqad  2516  eueq3  2940  ssnpss  3279  psstr  3280  elndif  3300  n0i  3460  axnulALT  4147  nfcvb  4205  zfpair  4212  onssneli  4502  nlimsucg  4633  onxpdisj  4769  reldmtpos  6242  bren2  6892  sdom0  6993  domunsn  7011  sdom1  7062  enp1i  7093  alephval3  7737  dfac2  7757  cdainflem  7817  ackbij1lem18  7863  isfin4-3  7941  fincssdom  7949  fin23lem41  7978  fin45  8018  fin17  8020  fin1a2lem7  8032  axcclem  8083  pwcfsdom  8205  canthp1lem1  8274  hargch  8299  winainflem  8315  renfdisj  8885  ltxrlt  8893  xmullem2  10585  rexmul  10591  xlemul1a  10608  fzdisj  10817  frgpcyg  16527  dvlog2lem  19999  lgsval2lem  20545  strlem1  22830  chrelat2i  22945  dfrdg4  24488  dvreasin  24923  finminlem  26231  psgnunilem3  27419  stoweidlem14  27763  isusgra0  28106  ax12-4  29106  ax12conj2  29108  a12study8  29119  a12study  29132  ax9lem7  29146  ax9lem12  29151  ax9lem15  29154  hlrelat2  29592  cdleme50ldil  30737
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator