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  3040  spc2d  3571  npss  4079  snprc  4684  dffv2  6959  kmlem3  10113  axpowndlem3  10559  nnunb  12445  rpnnen2lem12  16200  dsmmacl  21657  ntreq0  22971  noetasuplem4  27655  noetainflem4  27659  largei  32203  ballotlem2  34487  dffr5  35748  brsset  35884  brtxpsd  35889  dfrecs2  35945  dfint3  35947  con1bii2  37327  notbinot1  38080  elpadd0  39810  pm10.252  44357  pm10.253  44358  ralfal  45162