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  953  3anor  1075  3oran  1077  2nexaln  1797  nnel  2935  npss  3750  symdifass  3886  dfnul3  3951  snprc  4285  dffv2  6310  kmlem3  9012  axpowndlem3  9459  nnunb  11326  rpnnen2lem12  14998  dsmmacl  20133  ntreq0  20929  largei  29254  spc2d  29441  ballotlem2  30678  dffr5  31769  noetalem3  31990  brsset  32121  brtxpsd  32126  dfrecs2  32182  dfint3  32184  con1bii2  33309  notbinot1  34008  elpadd0  35413  pm10.252  38877  pm10.253  38878  2exanali  38904