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  2112  rexim  2622  ralf0  3535  dfon2lem9  23516  hbntg  23531  naim1  24198  naim2  24199  lukshef-ax2  24229  stoweidlem35  27119  vk15.4j  27344  tratrb  27352  hbntal  27372  tratrbVD  27687  con5VD  27726  vk15.4jVD  27740  ax12o10lem7K  28209  ax12o10lem7X  28210  ax12o10lem10K  28214  ax12o10lem10X  28216  ax12olem16K  28228  ax12olem16X  28229  ax10lem24X  28260  ax10lem17ALT  28290  ax9lem4  28310  ax9lem9  28315  ax9lem17  28323  cvrexchlem  28775  cvratlem  28777
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator