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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xor  1032  3anor  1125  3oran  1126  2nexaln  1863  2exanali  1893  nnel  3077  spc2d  3564  npss  4071  snprc  4688  dffv2  6983  kmlem3  10155  axpowndlem3  10602  nnunb  12518  rpnnen2lem12  16306  dsmmacl  21928  ntreq0  23271  noetasuplem4  27937  noetainflem4  27941  largei  32656  ballotlem2  34911  rankscottu  35547  dffr5  36267  brsset  36400  brtxpsd  36405  dfrecs2  36463  dfint3  36465  con1bii2  38019  notbinot1  38771  elpadd0  40624  pm10.252  45112  pm10.253  45113  ralfal  45920