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  1429  nic-axALT  1430  exim  1563  hbimd  1722  hbnt  1725  equsalhw  1731  nfnd  1761  dvelimv  1880  ax9o  1891  ax11indn  2135  rexim  2648  ralf0  3561  dfon2lem9  23548  hbntg  23563  naim1  24230  naim2  24231  lukshef-ax2  24261  stoweidlem35  27183  vk15.4j  27562  tratrb  27570  hbntal  27590  tratrbVD  27905  con5VD  27944  vk15.4jVD  27958  ax10lem17ALT  28390  ax9lem4  28410  ax9lem9  28415  ax9lem17  28423  cvrexchlem  28875  cvratlem  28877
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator