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.8wOLD  1678  hba1w  1693  ax5o  1729  19.8a  1730  hba1  1731  spimeh  1734  ax12olem3  1882  spime  1929  sbn  2015  spsbe  2028  hba1-o  2101  festino  2261  calemes  2271  fresison  2273  calemos  2274  fesapo  2275  necon3ai  2499  necon2bi  2505  necon4ai  2518  neneqad  2529  eueq3  2953  ssnpss  3292  psstr  3293  elndif  3313  n0i  3473  axnulALT  4163  nfcvb  4221  zfpair  4228  onssneli  4518  nlimsucg  4649  onxpdisj  4785  reldmtpos  6258  bren2  6908  sdom0  7009  domunsn  7027  sdom1  7078  enp1i  7109  alephval3  7753  dfac2  7773  cdainflem  7833  ackbij1lem18  7879  isfin4-3  7957  fincssdom  7965  fin23lem41  7994  fin45  8034  fin17  8036  fin1a2lem7  8048  axcclem  8099  pwcfsdom  8221  canthp1lem1  8290  hargch  8315  winainflem  8331  renfdisj  8901  ltxrlt  8909  xmullem2  10601  rexmul  10607  xlemul1a  10624  fzdisj  10833  frgpcyg  16543  dvlog2lem  20015  lgsval2lem  20561  strlem1  22846  chrelat2i  22961  dfrdg4  24560  dvreasin  25026  finminlem  26334  psgnunilem3  27522  stoweidlem14  27866  alneu  28082  isusgra0  28238  ax12olem3aAUX7  29434  spimeNEW7  29486  sbnNEW7  29537  spsbeNEW7  29546  ax12-4  29728  ax12conj2  29730  a12study8  29741  a12study  29754  ax9lem7  29768  ax9lem12  29773  ax9lem15  29776  hlrelat2  30214  cdleme50ldil  31359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator