Theorem con1bii 345

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		notnotb 304	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2		con1bii.1	. . 3 ⊢ (¬ 𝜑 ↔ 𝜓)
3	1, 2	xchbinx 323	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
4	3	bicomi 214	1 ⊢ (¬ 𝜓 ↔ 𝜑)

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  346  xor  971  3anor  1097  3oran  1099  2nexaln  1898  nnel  3036  npss  3851  symdifass  3988  dfnul3  4053  snprc  4389  dffv2  6425  kmlem3  9158  axpowndlem3  9605  nnunb  11472  rpnnen2lem12  15145  dsmmacl  20279  ntreq0  21075  largei  29427  spc2d  29614  ballotlem2  30851  dffr5  31942  noetalem3  32163  brsset  32294  brtxpsd  32299  dfrecs2  32355  dfint3  32357  con1bii2  33482  notbinot1  34183  elpadd0  35590  pm10.252  39054  pm10.253  39055  2exanali  39081