Theorem con1bii 331

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 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  891  3oran  993  had0  1458  2nexaln  1638  necon1abiiOLD  2706  necon1bbiiOLD  2708  nnel  2788  npss  3599  dfnul3  3773  snprc  4078  dffv2  5931  kmlem3  8535  axpowndlem3  8978  axpowndlem3OLD  8979  nnunb  10797  rpnnen2  13836  dsmmacl  18645  ntreq0  19451  largei  27058  spc2d  27245  ballotlem2  28300  dffr5  29157  symdifass  29452  brsset  29514  brtxpsd  29519  tfrqfree  29576  dfint3  29577  notbinot1  30451  pm10.252  31220  pm10.253  31221  2exanali  31247  elpadd0  35273