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

Theorem con3 126
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 19 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21con3d 125 1  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.65  164  con34b  283  nic-ax  1428  nic-axALT  1429  exim  1562  hbimd  1721  hbnt  1724  equsalhw  1730  nfnd  1760  dvelimv  1879  ax9o  1890  ax11indn  2134  rexim  2647  ralf0  3560  dfon2lem9  24147  hbntg  24162  naim1  24823  naim2  24824  lukshef-ax2  24854  stoweidlem35  27784  vk15.4j  28291  tratrb  28299  hbntal  28319  tratrbVD  28637  con5VD  28676  vk15.4jVD  28690  ax10lem17ALT  29123  ax9lem4  29143  ax9lem9  29148  ax9lem17  29156  cvrexchlem  29608  cvratlem  29610
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator