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  stoweidlem35  26918  vk15.4j  27081  tratrb  27089  hbntal  27109  tratrbVD  27424  con5VD  27463  vk15.4jVD  27477  ax12o10lem7K  27946  ax12o10lem7X  27947  ax12o10lem10K  27951  ax12o10lem10X  27953  ax12olem16K  27965  ax12olem16X  27966  ax10lem24X  27997  ax10lem17ALT  28027  ax9lem4  28047  ax9lem9  28052  ax9lem17  28060  cvrexchlem  28512  cvratlem  28514
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator