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  1017  3anor  1108  3oran  1109  2nexaln  1832  2exanali  1862  nnel  3047  spc2d  3558  npss  4067  snprc  4676  dffv2  6937  kmlem3  10075  axpowndlem3  10522  nnunb  12409  rpnnen2lem12  16162  dsmmacl  21708  ntreq0  23033  noetasuplem4  27716  noetainflem4  27720  largei  32354  ballotlem2  34666  dffr5  35967  brsset  36100  brtxpsd  36105  dfrecs2  36163  dfint3  36165  con1bii2  37584  notbinot1  38327  elpadd0  40182  pm10.252  44714  pm10.253  44715  ralfal  45517