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

Assertion

Ref	Expression
con1bii

Proof of Theorem con1bii

Step	Hyp	Ref	Expression
1		notnot 291	. . 3
2		con1bii.1	. . 3
3	1, 2	xchbinx 310	. 2
4	3	bicomi 202	1

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

This theorem is referenced by:  con2bii  332  xor  891  3oran  992  had0  1471  2nexaln  1651  necon1abiiOLD  2720  necon1bbiiOLD  2722  nnel  2802  npss  3613  dfnul3  3787  snprc  4093  dffv2  5946  kmlem3  8553  axpowndlem3  8996  axpowndlem3OLD  8997  nnunb  10816  rpnnen2  13959  dsmmacl  18772  ntreq0  19578  largei  27186  spc2d  27373  ballotlem2  28427  dffr5  29182  symdifass  29477  brsset  29539  brtxpsd  29544  tfrqfree  29601  dfint3  29602  notbinot1  30476  pm10.252  31266  pm10.253  31267  2exanali  31293  elpadd0  35533

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