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

Theorem con34b 292
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  339  pm4.14  578  raldifsni  4105  weniso  6146  dfom2  6580  dfsup2  7795  wemapsolem  7867  pwfseqlem3  8930  indstr  11026  rpnnen2  13612  algcvgblem  13856  isirred2  16901  isdomn2  17479  ist0-3  19067  mdegleb  21653  dchrelbas4  22700  toslublem  26264  tosglblem  26266  tsbi3  29086  isdomn3  29712  conss34  29838  dff14a  30284
  Copyright terms: Public domain W3C validator