Theorem con1bii 358

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  xor  1027  3anor  1119  3oran  1120  2nexaln  1849  2exanali  1879  nnel  3070  spc2d  3560  npss  4065  snprc  4673  dffv2  6956  kmlem3  10102  axpowndlem3  10550  nnunb  12470  rpnnen2lem12  16247  dsmmacl  21780  ntreq0  23124  noetasuplem4  27787  noetainflem4  27791  largei  32426  ballotlem2  34746  dffr5  36064  brsset  36197  brtxpsd  36202  dfrecs2  36260  dfint3  36262  con1bii2  37786  notbinot1  38538  elpadd0  40393  pm10.252  44897  pm10.253  44898  ralfal  45699