Theorem con1bii 333

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 293	. . 3 |- ( ph <-> -. -. ph )
2		con1bii.1	. . 3 |- ( -. ph <-> ps )
3	1, 2	xchbinx 312	. 2 |- ( ph <-> -. ps )
4	3	bicomi 206	1 |- ( -. ps <-> ph )

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

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 189

This theorem is referenced by:  con2bii  334  xor  902  3oran  1004  2nexaln  1702  nnel  2733  npss  3543  symdifass  3672  dfnul3  3734  snprc  4035  dffv2  5938  kmlem3  8582  axpowndlem3  9024  nnunb  10865  rpnnen2  14278  dsmmacl  19304  ntreq0  20093  largei  27920  spc2d  28107  ballotlem2  29321  dffr5  30393  brsset  30656  brtxpsd  30661  dfrecs2  30717  dfint3  30719  con1bii2  31734  notbinot1  32312  elpadd0  33374  pm10.252  36710  pm10.253  36711  2exanali  36737