Theorem con1bii 340

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

Syntax hints:  ¬ wn 3   ↔ wb 191

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 192

This theorem is referenced by:  con2bii  341  xor  921  3oran  1040  2nexaln  1733  nnel  2787  npss  3565  symdifass  3699  dfnul3  3760  snprc  4064  dffv2  6005  kmlem3  8667  axpowndlem3  9109  nnunb  10956  rpnnen2  14438  dsmmacl  19462  ntreq0  20250  largei  28083  spc2d  28270  ballotlem2  29475  dffr5  30544  brsset  30807  brtxpsd  30812  dfrecs2  30868  dfint3  30870  con1bii2  31955  notbinot1  32549  elpadd0  33614  pm10.252  37067  pm10.253  37068  2exanali  37094