Theorem con1bii 359

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  xor  1032  3anor  1125  3oran  1126  2nexaln  1860  2exanali  1890  nnel  3074  spc2d  3562  npss  4069  snprc  4684  dffv2  6978  kmlem3  10137  axpowndlem3  10585  nnunb  12501  rpnnen2lem12  16282  dsmmacl  21872  ntreq0  23215  noetasuplem4  27881  noetainflem4  27885  largei  32600  ballotlem2  34860  rankscottu  35504  dffr5  36227  brsset  36360  brtxpsd  36365  dfrecs2  36423  dfint3  36425  con1bii2  37959  notbinot1  38711  elpadd0  40564  pm10.252  45054  pm10.253  45055  ralfal  45862