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  hbnt  1783  nfndOLD  1800  hbimdOLD  1825  equsalhwOLD  1851  ax9o  1943  dvelimvOLD  1990  ax11indn  2231  rexim  2755  ralf0  3679  dfon2lem9  25173  hbntg  25188  naim1  25850  naim2  25851  lukshef-ax2  25881  vk15.4j  27957  tratrb  27965  hbntal  27985  tratrbVD  28316  con5VD  28355  vk15.4jVD  28369  dvelimvNEW7  28802  ax9oNEW7  28809  cvrexchlem  29535  cvratlem  29537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator