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

Theorem con1bii 333
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypothesis
Ref Expression
con1bii.1  |-  ( -. 
ph 
<->  ps )
Assertion
Ref Expression
con1bii  |-  ( -. 
ps 
<-> 
ph )

Proof of Theorem con1bii
StepHypRef Expression
1 notnot 293 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 312 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 206 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> 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:  con2bii  334  xor  900  3oran  1002  2nexaln  1699  necon1abiiOLD  2688  necon1bbiiOLD  2690  nnel  2771  npss  3576  symdifass  3703  dfnul3  3765  snprc  4061  dffv2  5952  kmlem3  8584  axpowndlem3  9026  nnunb  10867  rpnnen2  14271  dsmmacl  19296  ntreq0  20085  largei  27912  spc2d  28099  ballotlem2  29323  dffr5  30394  brsset  30655  brtxpsd  30660  dfrecs2  30716  dfint3  30718  notbinot1  32232  elpadd0  33299  pm10.252  36574  pm10.253  36575  2exanali  36601
  Copyright terms: Public domain W3C validator