Theorem con1bii 360

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  1012  3anor  1105  3oran  1106  2nexaln  1831  2exanali  1861  nnel  3100  spc2d  3551  npss  4038  dfnul3  4246  snprc  4613  dffv2  6733  kmlem3  9563  axpowndlem3  10010  nnunb  11881  rpnnen2lem12  15570  dsmmacl  20430  ntreq0  21682  largei  30050  ballotlem2  31856  dffr5  33102  noetalem3  33332  brsset  33463  brtxpsd  33468  dfrecs2  33524  dfint3  33526  con1bii2  34749  notbinot1  35517  elpadd0  37105  pm10.252  41065  pm10.253  41066