MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con3 Structured version   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  1447  nic-axALT  1448  exim  1584  hbntOLD  1800  nfndOLD  1810  hbimdOLD  1835  equsalhwOLD  1861  ax9o  1954  dvelimvOLD  2028  ax11indn  2271  rexim  2802  ralf0  3726  dfon2lem9  25410  hbntg  25425  naim1  26126  naim2  26127  lukshef-ax2  26157  vk15.4j  28549  tratrb  28557  hbntal  28577  tratrbVD  28910  con5VD  28949  vk15.4jVD  28963  dvelimvNEW7  29399  ax9oNEW7  29406  cvrexchlem  30153  cvratlem  30155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator