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 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  1701  hba1w  1718  ax5o  1761  19.8aOLD  1768  hba1OLD  1801  spimehOLD  1836  spimeOLD  1957  ax12olem3OLD  1979  sbn  2111  spsbe  2124  hba1-o  2199  festino  2359  calemes  2369  fresison  2371  calemos  2372  fesapo  2373  necon3ai  2607  necon2bi  2613  necon4ai  2626  neneqad  2637  eueq3  3069  ssnpss  3410  psstr  3411  elndif  3431  n0i  3593  axnulALT  4296  nfcvb  4354  zfpair  4361  onssneli  4650  nlimsucg  4781  onxpdisj  4916  funtpg  5460  ftpg  5875  reldmtpos  6446  bren2  7097  sdom0  7198  domunsn  7216  sdom1  7267  enp1i  7302  alephval3  7947  dfac2  7967  cdainflem  8027  ackbij1lem18  8073  isfin4-3  8151  fincssdom  8159  fin23lem41  8188  fin45  8228  fin17  8230  fin1a2lem7  8242  axcclem  8293  pwcfsdom  8414  canthp1lem1  8483  hargch  8508  winainflem  8524  renfdisj  9094  ltxrlt  9102  xmullem2  10800  rexmul  10806  xlemul1a  10823  fzdisj  11034  frgpcyg  16809  dvlog2lem  20496  lgsval2lem  21043  isusgra0  21329  cusgrares  21434  2pthlem2  21549  strlem1  23706  chrelat2i  23821  dfrdg4  25703  dvreasin  26179  finminlem  26211  psgnunilem3  27287  stoweidlem14  27630  alneu  27846  2spot0  28167  ax12olem3aAUX7  29163  spimeNEW7  29215  sbnNEW7  29266  spsbeNEW7  29275  hlrelat2  29885  cdleme50ldil  31030
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator