Theorem con1bii 357

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xor  1012  3anor  1107  3oran  1108  2nexaln  1832  2exanali  1863  nnel  3058  spc2d  3541  npss  4045  dfnul3OLD  4262  snprc  4653  dffv2  6863  kmlem3  9908  axpowndlem3  10355  nnunb  12229  rpnnen2lem12  15934  dsmmacl  20948  ntreq0  22228  largei  30629  ballotlem2  32455  dffr5  33721  noetasuplem4  33939  noetainflem4  33943  brsset  34191  brtxpsd  34196  dfrecs2  34252  dfint3  34254  con1bii2  35503  notbinot1  36237  elpadd0  37823  pm10.252  41979  pm10.253  41980