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  1565  hbimd  1733  hbnt  1736  equsalhw  1742  nfnd  1772  dvelimv  1892  ax9o  1903  ax11indn  2147  rexim  2660  ralf0  3573  dfon2lem9  24218  hbntg  24233  naim1  24895  naim2  24896  lukshef-ax2  24926  stoweidlem35  27887  vk15.4j  28590  tratrb  28598  hbntal  28618  tratrbVD  28953  con5VD  28992  vk15.4jVD  29006  dvelimvNEW7  29439  ax9oNEW7  29446  ax10lem17ALT  29745  ax9lem4  29765  ax9lem9  29770  ax9lem17  29778  cvrexchlem  30230  cvratlem  30232
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator