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

Theorem con2i 115
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 114 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  nsyl  116  notnot1  117  pm2.65i  168  pm3.14  490  pclem6  898  19.8wOLD  1706  hba1w  1723  ax5o  1766  19.8aOLD  1773  hba1OLD  1806  spimehOLD  1841  spimeOLD  1960  ax12olem3OLD  2014  sbnOLD  2133  spsbeOLD  2149  hba1-o  2228  festino  2388  calemes  2398  fresison  2400  calemos  2401  fesapo  2402  necon3ai  2646  necon2bi  2652  necon4ai  2665  neneqad  2676  eueq3  3111  ssnpss  3452  psstr  3453  elndif  3473  n0i  3635  axnulALT  4338  nfcvb  4396  zfpair  4403  onssneli  4693  nlimsucg  4824  onxpdisj  4959  funtpg  5503  ftpg  5918  reldmtpos  6489  bren2  7140  sdom0  7241  domunsn  7259  sdom1  7310  enp1i  7345  alephval3  7993  dfac2  8013  cdainflem  8073  ackbij1lem18  8119  isfin4-3  8197  fincssdom  8205  fin23lem41  8234  fin45  8274  fin17  8276  fin1a2lem7  8288  axcclem  8339  pwcfsdom  8460  canthp1lem1  8529  hargch  8554  winainflem  8570  renfdisj  9140  ltxrlt  9148  xmullem2  10846  rexmul  10852  xlemul1a  10869  fzdisj  11080  frgpcyg  16856  dvlog2lem  20545  lgsval2lem  21092  isusgra0  21378  cusgrares  21483  2pthlem2  21598  strlem1  23755  chrelat2i  23870  dfrdg4  25797  dvreasin  26292  finminlem  26323  psgnunilem3  27398  stoweidlem14  27741  alneu  27957  2spot0  28515  ax12olem3aAUX7  29519  spimeNEW7  29571  sbnNEW7  29624  spsbeNEW7  29633  hlrelat2  30262  cdleme50ldil  31407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator