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 20 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21con3d 127 1  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.65  166  con34b  284  nic-ax  1444  nic-axALT  1445  exim  1581  hbntOLD  1796  nfndOLD  1806  hbimdOLD  1831  equsalhwOLD  1857  ax9o  1950  dvelimvOLD  1994  ax11indn  2253  rexim  2778  ralf0  3702  dfon2lem9  25369  hbntg  25384  naim1  26046  naim2  26047  lukshef-ax2  26077  vk15.4j  28331  tratrb  28339  hbntal  28359  tratrbVD  28691  con5VD  28730  vk15.4jVD  28744  dvelimvNEW7  29180  ax9oNEW7  29187  cvrexchlem  29913  cvratlem  29915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator