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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  xor  1011  3anor  1104  3oran  1105  2nexaln  1826  2exanali  1856  nnel  3132  spc2d  3602  npss  4086  dfnul3  4294  snprc  4652  dffv2  6755  kmlem3  9577  axpowndlem3  10020  nnunb  11892  rpnnen2lem12  15577  dsmmacl  20884  ntreq0  21684  largei  30043  ballotlem2  31746  dffr5  32989  noetalem3  33219  brsset  33350  brtxpsd  33355  dfrecs2  33411  dfint3  33413  con1bii2  34612  notbinot1  35356  elpadd0  36944  pm10.252  40691  pm10.253  40692