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  1016  3anor  1107  3oran  1108  2nexaln  1830  2exanali  1860  nnel  3039  spc2d  3559  npss  4066  snprc  4671  dffv2  6922  kmlem3  10066  axpowndlem3  10512  nnunb  12398  rpnnen2lem12  16152  dsmmacl  21666  ntreq0  22980  noetasuplem4  27664  noetainflem4  27668  largei  32229  ballotlem2  34456  dffr5  35726  brsset  35862  brtxpsd  35867  dfrecs2  35923  dfint3  35925  con1bii2  37305  notbinot1  38058  elpadd0  39788  pm10.252  44334  pm10.253  44335  ralfal  45139