Theorem con1bii 359

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 318	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2		con1bii.1	. . 3 ⊢ (¬ 𝜑 ↔ 𝜓)
3	1, 2	xchbinx 337	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
4	3	bicomi 227	1 ⊢ (¬ 𝜓 ↔ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xor  1032  3anor  1125  3oran  1126  2nexaln  1862  2exanali  1892  nnel  3071  spc2d  3556  npss  4041  snprc  4677  dffv2  6980  kmlem3  10231  axpowndlem3  10684  nnunb  12602  rpnnen2lem12  16393  dsmmacl  22047  ntreq0  23395  noetasuplem4  28093  noetainflem4  28097  largei  32869  ballotlem2  35163  rankscottu  35795  dffr5  36561  brsset  36693  brtxpsd  36698  dfrecs2  36756  dfint3  36758  con1bii2  38298  notbinot1  39056  elpadd0  40909  pm10.252  45387  pm10.253  45388  ralfal  46218