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

Theorem con2i 120
Description: A contraposition inference. Its associated inference is mt2 179. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. 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 22 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 119 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  nsyl  121  notnot1  122  pm2.65i  173  pm3.14  502  pclem6  930  hba1w  1800  axc4  1846  hba1-o  2214  festino  2390  calemes  2400  fresison  2402  calemos  2403  fesapo  2404  necon3ai  2671  necon2ai  2678  necon2bi  2680  necon4aiOLD  2682  neneqadOLD  2752  eueq3  3260  ssnpss  3592  psstr  3593  elndif  3613  n0i  3775  axnulALT  4564  nfcvb  4667  zfpair  4674  onssneli  4977  onxpdisj  5073  funtpg  5628  ftpg  6066  nlimsucg  6662  reldmtpos  6965  bren2  7548  sdom0  7651  domunsn  7669  sdom1  7721  enp1i  7757  alephval3  8494  dfac2  8514  cdainflem  8574  ackbij1lem18  8620  isfin4-3  8698  fincssdom  8706  fin23lem41  8735  fin45  8775  fin17  8777  fin1a2lem7  8789  axcclem  8840  pwcfsdom  8961  canthp1lem1  9033  hargch  9054  winainflem  9074  ltxrlt  9658  xmullem2  11468  rexmul  11474  xlemul1a  11491  fzdisj  11723  pmtrdifellem4  16483  psgnunilem3  16500  frgpcyg  18590  dvlog2lem  23011  lgsval2lem  23559  isusgra0  24325  usgraop  24328  cusgrares  24450  2pthlem2  24576  2spot0  25042  strlem1  27147  chrelat2i  27262  dfrdg4  29576  finminlem  30112  stoweidlem14  31750  alneu  32160  2nodd  32453  bj-nimn  34011  hlrelat2  35002  cdleme50ldil  36149
  Copyright terms: Public domain W3C validator