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  3046  spc2d  3544  npss  4053  snprc  4661  dffv2  6935  kmlem3  10075  axpowndlem3  10522  nnunb  12433  rpnnen2lem12  16192  dsmmacl  21721  ntreq0  23042  noetasuplem4  27700  noetainflem4  27704  largei  32338  ballotlem2  34633  dffr5  35936  brsset  36069  brtxpsd  36074  dfrecs2  36132  dfint3  36134  con1bii2  37648  notbinot1  38400  elpadd0  40255  pm10.252  44788  pm10.253  44789  ralfal  45591