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

Theorem con34b 294
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 140 . 2  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
2 ax-3 8 . 2  |-  ( ( -.  ps  ->  -.  ph )  ->  ( ph  ->  ps ) )
31, 2impbii 191 1  |-  ( (
ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  mtt  341  pm4.14  581  19.23t  1965  r19.23v  2906  raldifsni  4128  dff14a  6183  weniso  6258  dfom2  6706  dfsup2  7962  wemapsolem  8069  pwfseqlem3  9087  indstr  11229  rpnnen2  14271  algcvgblem  14529  isirred2  17922  isdomn2  18516  ist0-3  20353  mdegleb  23005  dchrelbas4  24163  toslublem  28429  tosglblem  28431  poimirlem25  31923  poimirlem30  31928  tsbi3  32335  isdomn3  36045  conss34  36697  aacllem  39884
  Copyright terms: Public domain W3C validator