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  3309  disjsn  3693  oneqmini  4443  kmlem4  7779  isprm3  12767  pm13.196a  27614  stoweidlem34  27783  bnj1171  29030  bnj1176  29035  bnj1204  29042  bnj1388  29063  bnj1523  29101
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