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

Theorem notbi 286
Description: Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)
Assertion
Ref Expression
notbi  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )

Proof of Theorem notbi
StepHypRef Expression
1 id 19 . . 3  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21notbid 285 . 2  |-  ( (
ph 
<->  ps )  ->  ( -.  ph  <->  -.  ps )
)
3 id 19 . . 3  |-  ( ( -.  ph  <->  -.  ps )  ->  ( -.  ph  <->  -.  ps )
)
43con4bid 284 . 2  |-  ( ( -.  ph  <->  -.  ps )  ->  ( ph  <->  ps )
)
52, 4impbii 180 1  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  notbii  287  con4bii  288  con2bi  318  nbn2  334  pm5.32  617  cbvexd  1962  isocnv3  5845  symdifass  24442  onsuct0  24952  f1omvdco3  27495  bothfbothsame  27971  aisbnaxb  27982  cbvexdOLD7  29689
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