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

Theorem con3 128
Description: Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
Assertion
Ref Expression
con3  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )

Proof of Theorem con3
StepHypRef Expression
1 id 21 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21con3d 127 1  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  pm2.65  166  con34b  285  nic-ax  1433  nic-axALT  1434  exim  1573  ax12o10lem7  1641  ax12o10lem10  1644  ax12olem16  1650  ax10lem24  1673  hbnt  1717  nfnd  1726  ax9o  1814  ax11indn  2108  rexim  2609  ralf0  3466  dfon2lem9  23315  hbntg  23330  naim1  23997  naim2  23998  lukshef-ax2  24028  vk15.4j  26984  tratrb  26992  hbntal  27012  tratrbVD  27327  con5VD  27366  vk15.4jVD  27380  ax10lem17ALT  27812  ax9lem4  27832  ax9lem9  27837  ax9lem17  27845  cvrexchlem  28297  cvratlem  28299
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator