MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con34b Structured version   Unicode version

Theorem con34b 290
Description: Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
con34b  |-  ( (
ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) )

Proof of Theorem con34b
StepHypRef Expression
1 con3 134 . 2  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
2 ax-3 8 . 2  |-  ( ( -.  ps  ->  -.  ph )  ->  ( ph  ->  ps ) )
31, 2impbii 188 1  |-  ( (
ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  mtt  337  pm4.14  576  r19.23v  2934  raldifsni  4146  dff14a  6152  weniso  6225  dfom2  6675  dfsup2  7894  wemapsolem  7967  pwfseqlem3  9027  indstr  11151  rpnnen2  14043  algcvgblem  14290  isirred2  17545  isdomn2  18143  ist0-3  20013  mdegleb  22630  dchrelbas4  23716  toslublem  27889  tosglblem  27891  tsbi3  30782  isdomn3  31405  conss34  31592  aacllem  33604
  Copyright terms: Public domain W3C validator