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  3545  npss  4054  snprc  4662  dffv2  6929  kmlem3  10066  axpowndlem3  10513  nnunb  12424  rpnnen2lem12  16183  dsmmacl  21731  ntreq0  23052  noetasuplem4  27714  noetainflem4  27718  largei  32353  ballotlem2  34649  dffr5  35952  brsset  36085  brtxpsd  36090  dfrecs2  36148  dfint3  36150  con1bii2  37662  notbinot1  38414  elpadd0  40269  pm10.252  44806  pm10.253  44807  ralfal  45609