Theorem con1bii 356

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 224	1 ⊢ (¬ 𝜓 ↔ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  xor  1015  3anor  1108  3oran  1109  2nexaln  1828  2exanali  1859  nnel  3062  spc2d  3615  npss  4136  dfnul3OLD  4358  snprc  4742  dffv2  7017  kmlem3  10222  axpowndlem3  10668  nnunb  12549  rpnnen2lem12  16273  dsmmacl  21784  ntreq0  23106  noetasuplem4  27799  noetainflem4  27803  largei  32299  ballotlem2  34453  dffr5  35716  brsset  35853  brtxpsd  35858  dfrecs2  35914  dfint3  35916  con1bii2  37298  notbinot1  38039  elpadd0  39766  pm10.252  44330  pm10.253  44331  ralfal  45066