Theorem con1bii 346

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		notnotb 304	. . 3 |- ( ph <-> -. -. ph )
2		con1bii.1	. . 3 |- ( -. ph <-> ps )
3	1, 2	xchbinx 324	. 2 |- ( ph <-> -. ps )
4	3	bicomi 214	1 |- ( -. ps <-> ph )

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

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 197

This theorem is referenced by:  con2bii  347  xor  935  3oran  1057  2nexaln  1757  nnel  2906  npss  3717  symdifass  3853  dfnul3  3918  snprc  4253  dffv2  6271  kmlem3  8974  axpowndlem3  9421  nnunb  11288  rpnnen2lem12  14954  dsmmacl  20085  ntreq0  20881  largei  29126  spc2d  29313  ballotlem2  30550  dffr5  31643  noetalem3  31865  brsset  31996  brtxpsd  32001  dfrecs2  32057  dfint3  32059  con1bii2  33179  notbinot1  33878  elpadd0  35095  pm10.252  38560  pm10.253  38561  2exanali  38587