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  1862  2exanali  1892  nnel  3071  spc2d  3556  npss  4041  snprc  4674  dffv2  6980  kmlem3  10234  axpowndlem3  10687  nnunb  12605  rpnnen2lem12  16398  dsmmacl  22052  ntreq0  23400  noetasuplem4  28098  noetainflem4  28102  largei  32874  ballotlem2  35167  rankscottu  35807  dffr5  36611  brsset  36743  brtxpsd  36748  dfrecs2  36806  dfint3  36808  con1bii2  38348  notbinot1  39106  elpadd0  40959  pm10.252  45438  pm10.253  45439  ralfal  46269