Theorem con1bii 344

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

Syntax hints:  ¬ wn 3   ↔ wb 194

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 195

This theorem is referenced by:  con2bii  345  xor  930  3oran  1049  2nexaln  1735  nnel  2796  npss  3583  symdifass  3718  dfnul3  3780  snprc  4100  dffv2  6064  kmlem3  8732  axpowndlem3  9175  nnunb  11042  rpnnen2lem12  14660  dsmmacl  19805  ntreq0  20592  largei  28299  spc2d  28486  ballotlem2  29685  dffr5  30739  brsset  31002  brtxpsd  31007  dfrecs2  31063  dfint3  31065  con1bii2  32187  notbinot1  32923  elpadd0  33988  pm10.252  37464  pm10.253  37465  2exanali  37491