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

Step	Hyp	Ref	Expression
1		notnot 293	. . 3 |- ( ph <-> -. -. ph )
2		con1bii.1	. . 3 |- ( -. ph <-> ps )
3	1, 2	xchbinx 312	. 2 |- ( ph <-> -. ps )
4	3	bicomi 206	1 |- ( -. ps <-> ph )

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