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

Theorem con2i 123
Description: A contraposition inference. Its associated inference is mt2 182. (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 122 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  124  notnot1  125  pm2.65i  176  pm3.14  504  pclem6  938  hba1w  1868  axc4  1915  festino  2370  calemes  2380  fresison  2382  calemos  2383  fesapo  2384  necon3ai  2648  necon2ai  2655  necon2bi  2657  necon4aiOLD  2659  neneqadOLD  2729  eueq3  3245  ssnpss  3568  psstr  3569  elndif  3589  n0i  3766  axnulALT  4552  nfcvb  4651  zfpair  4658  onssneli  5551  onxpdisj  5561  funtpg  5651  ftpg  6089  nlimsucg  6683  reldmtpos  6992  bren2  7610  sdom0  7713  domunsn  7731  sdom1  7781  enp1i  7815  alephval3  8548  dfac2  8568  cdainflem  8628  ackbij1lem18  8674  isfin4-3  8752  fincssdom  8760  fin23lem41  8789  fin45  8829  fin17  8831  fin1a2lem7  8843  axcclem  8894  pwcfsdom  9015  canthp1lem1  9084  hargch  9105  winainflem  9125  ltxrlt  9711  xmullem2  11558  rexmul  11564  xlemul1a  11581  fzdisj  11833  lcmfunsnlem2lem2  14611  pmtrdifellem4  17119  psgnunilem3  17136  frgpcyg  19142  dvlog2lem  23595  lgsval2lem  24232  isusgra0  25072  usgraop  25075  cusgrares  25198  2pthlem2  25324  2spot0  25790  strlem1  27901  chrelat2i  28016  dfrdg4  30723  finminlem  30979  bj-nimn  31143  finxpreclem3  31749  finxpreclem5  31751  hba1-o  32438  hlrelat2  32937  cdleme50ldil  34084  stoweidlem14  37814  alneu  38493  isusgr0  39037  2nodd  39432
  Copyright terms: Public domain W3C validator