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  3046  spc2d  3581  npss  4088  snprc  4693  dffv2  6974  kmlem3  10167  axpowndlem3  10613  nnunb  12497  rpnnen2lem12  16243  dsmmacl  21701  ntreq0  23015  noetasuplem4  27700  noetainflem4  27704  largei  32248  ballotlem2  34521  dffr5  35771  brsset  35907  brtxpsd  35912  dfrecs2  35968  dfint3  35970  con1bii2  37350  notbinot1  38103  elpadd0  39828  pm10.252  44385  pm10.253  44386  ralfal  45185