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 21 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 113 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  nsyl  115  notnot1  116  pm2.65i  167  pm3.14  490  pclem6  901  ax12o10lem4  1638  ax12o10lem5  1639  ax12o10lem8  1642  ax12olem23  1657  ax5o  1693  hba1  1718  19.8a  1758  a4ime  1869  sbn  1955  a4sbe  1968  festino  2223  calemes  2233  fresison  2235  calemos  2236  fesapo  2237  necon3ai  2461  necon2bi  2467  necon4ai  2480  neneqad  2491  eueq3  2915  ssnpss  3254  psstr  3255  elndif  3275  n0i  3435  nfcvb  4177  zfpair  4184  onssneli  4474  nlimsucg  4605  onxpdisj  4757  reldmtpos  6176  bren2  6860  sdom0  6961  domunsn  6979  sdom1  7030  enp1i  7061  alephval3  7705  dfac2  7725  cdainflem  7785  ackbij1lem18  7831  isfin4-3  7909  fincssdom  7917  fin23lem41  7946  fin45  7986  fin17  7988  fin1a2lem7  8000  axcclem  8051  pwcfsdom  8173  canthp1lem1  8242  hargch  8267  winainflem  8283  renfdisj  8853  ltxrlt  8861  xmullem2  10551  rexmul  10557  xlemul1a  10574  fzdisj  10783  frgpcyg  16489  dvlog2lem  19961  lgsval2lem  20507  strlem1  22790  chrelat2i  22905  axfelem18  23732  axfelem22  23736  dfrdg4  23863  finminlem  25598  psgnunilem3  26786  stoweidlem14  27098  ax9dgenK  28174  hba1wK  28183  ax12o10lem4K  28203  ax12o10lem4X  28204  ax12o10lem5K  28205  ax12o10lem5X  28206  ax12o10lem8K  28211  ax12o10lem8X  28212  ax12olem23X  28244  ax12-4  28273  ax12conj2  28275  a12study8  28286  a12study  28299  ax9lem7  28313  ax9lem12  28318  ax9lem15  28321  hlrelat2  28759  cdleme50ldil  29904
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator