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

Theorem con2b 324
Description: Contraposition. Bidirectional version of con2 108. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
con2b  |-  ( (
ph  ->  -.  ps )  <->  ( ps  ->  -.  ph )
)

Proof of Theorem con2b
StepHypRef Expression
1 con2 108 . 2  |-  ( (
ph  ->  -.  ps )  ->  ( ps  ->  -.  ph ) )
2 con2 108 . 2  |-  ( ( ps  ->  -.  ph )  ->  ( ph  ->  -.  ps ) )
31, 2impbii 180 1  |-  ( (
ph  ->  -.  ps )  <->  ( ps  ->  -.  ph )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  mt2bi  328  pm4.15  564  nic-ax  1428  nic-axALT  1429  ssconb  3322  disjsn  3706  oneqmini  4459  kmlem4  7795  isprm3  12783  pm13.196a  27717  stoweidlem34  27886  bnj1171  29346  bnj1176  29351  bnj1204  29358  bnj1388  29379  bnj1523  29417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator