Theorem con1bii 357

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xor  1014  3anor  1109  3oran  1110  2nexaln  1833  2exanali  1864  nnel  3057  spc2d  3593  npss  4111  dfnul3OLD  4329  snprc  4722  dffv2  6987  kmlem3  10147  axpowndlem3  10594  nnunb  12468  rpnnen2lem12  16168  dsmmacl  21296  ntreq0  22581  noetasuplem4  27239  noetainflem4  27243  largei  31551  ballotlem2  33518  dffr5  34755  brsset  34892  brtxpsd  34897  dfrecs2  34953  dfint3  34955  con1bii2  36261  notbinot1  36995  elpadd0  38728  pm10.252  43168  pm10.253  43169  ralfal  43903