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  886  3oran  984  had0  1446  2nexaln  1622  necon1abiiOLD  2711  necon1bbiiOLD  2713  nnel  2793  npss  3564  dfnul3  3738  snprc  4037  dffv2  5863  kmlem3  8422  axpowndlem3  8865  axpowndlem3OLD  8866  nnunb  10676  rpnnen2  13610  dsmmacl  18275  ntreq0  18797  largei  25806  spc2d  25993  ballotlem2  27005  dffr5  27697  symdifass  27992  brsset  28054  brtxpsd  28059  tfrqfree  28116  dfint3  28117  notbinot1  29017  pm10.252  29751  pm10.253  29752  2exanali  29778  elpadd0  33759