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  3072  spc2d  3557  npss  4062  snprc  4678  dffv2  6972  kmlem3  10212  axpowndlem3  10665  nnunb  12583  rpnnen2lem12  16373  dsmmacl  22027  ntreq0  23375  noetasuplem4  28075  noetainflem4  28079  largei  32851  ballotlem2  35104  rankscottu  35731  dffr5  36488  brsset  36621  brtxpsd  36626  dfrecs2  36684  dfint3  36686  con1bii2  38223  notbinot1  38981  elpadd0  40834  pm10.252  45304  pm10.253  45305  ralfal  46119