Theorem con1bii 348

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

Syntax hints:  ¬ wn 3   ↔ wb 198

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 199

This theorem is referenced by:  con2bii  349  xor  1000  3anor  1095  3oran  1096  2nexaln  1873  nnel  3084  npss  3939  symdifassOLD  4077  dfnul3  4145  snprc  4484  dffv2  6533  kmlem3  9311  axpowndlem3  9758  nnunb  11642  rpnnen2lem12  15362  dsmmacl  20488  ntreq0  21293  largei  29702  spc2d  29889  ballotlem2  31153  dffr5  32241  noetalem3  32458  brsset  32589  brtxpsd  32594  dfrecs2  32650  dfint3  32652  con1bii2  33778  notbinot1  34507  elpadd0  35968  pm10.252  39526  pm10.253  39527  2exanali  39553