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  3073  spc2d  3559  npss  4065  snprc  4681  dffv2  6977  kmlem3  10159  axpowndlem3  10612  nnunb  12528  rpnnen2lem12  16319  dsmmacl  21960  ntreq0  23308  noetasuplem4  27980  noetainflem4  27984  largei  32756  ballotlem2  35008  rankscottu  35644  dffr5  36341  brsset  36474  brtxpsd  36479  dfrecs2  36537  dfint3  36539  con1bii2  38094  notbinot1  38837  elpadd0  40690  pm10.252  45193  pm10.253  45194  ralfal  46001