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  3568  npss  4076  snprc  4681  dffv2  6956  kmlem3  10106  axpowndlem3  10552  nnunb  12438  rpnnen2lem12  16193  dsmmacl  21650  ntreq0  22964  noetasuplem4  27648  noetainflem4  27652  largei  32196  ballotlem2  34480  dffr5  35741  brsset  35877  brtxpsd  35882  dfrecs2  35938  dfint3  35940  con1bii2  37320  notbinot1  38073  elpadd0  39803  pm10.252  44350  pm10.253  44351  ralfal  45155