Theorem con1bii 329

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 289	. . 3 |- ( ph <-> -. -. ph )
2		con1bii.1	. . 3 |- ( -. ph <-> ps )
3	1, 2	xchbinx 308	. 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  330  xor  889  3oran  990  had0  1475  2nexaln  1656  necon1abiiOLD  2717  necon1bbiiOLD  2719  nnel  2799  npss  3600  symdifass  3724  dfnul3  3786  snprc  4079  dffv2  5921  kmlem3  8523  axpowndlem3  8965  nnunb  10787  rpnnen2  14043  dsmmacl  18945  ntreq0  19745  largei  27384  spc2d  27571  ballotlem2  28691  dffr5  29423  brsset  29767  brtxpsd  29772  tfrqfree  29829  dfint3  29830  notbinot1  30716  pm10.252  31507  pm10.253  31508  2exanali  31534  elpadd0  35930