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  887  3oran  987  had0  1450  2nexaln  1626  necon1abiiOLD  2725  necon1bbiiOLD  2727  nnel  2807  npss  3609  dfnul3  3783  snprc  4086  dffv2  5933  kmlem3  8523  axpowndlem3  8966  axpowndlem3OLD  8967  nnunb  10782  rpnnen2  13811  dsmmacl  18534  ntreq0  19339  largei  26850  spc2d  27037  ballotlem2  28055  dffr5  28747  symdifass  29042  brsset  29104  brtxpsd  29109  tfrqfree  29166  dfint3  29167  notbinot1  30068  pm10.252  30801  pm10.253  30802  2exanali  30828  elpadd0  34482