Theorem con1bii 331

Description: A contraposition inference. (Contributed by NM, 5-Aug-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 291	. . 3 |- ( ph <-> -. -. ph )
2		con1bii.1	. . 3 |- ( -. ph <-> ps )
3	1, 2	xchbinx 310	. 2 |- ( ph <-> -. ps )
4	3	bicomi 202	1 |- ( -. ps <-> ph )

Syntax hints:   -. wn 3   <-> wb 184

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 185

This theorem is referenced by:  con2bii  332  xor  881  3oran  979  had0  1450  2nexaln  1626  necon1abii  2660  necon1bbii  2661  npss  3463  dfnul3  3637  snprc  3936  dffv2  5761  kmlem3  8317  axpowndlem3  8760  axpowndlem3OLD  8761  nnunb  10571  rpnnen2  13504  dsmmacl  18125  ntreq0  18640  largei  25606  spc2d  25793  ballotlem2  26801  dffr5  27492  symdifass  27787  brsset  27849  brtxpsd  27854  tfrqfree  27911  dfint3  27912  notbinot1  28804  pm10.252  29538  pm10.253  29539  2exanali  29565  elpadd0  33175