Theorem con1bii 356

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 314	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2		con1bii.1	. . 3 ⊢ (¬ 𝜑 ↔ 𝜓)
3	1, 2	xchbinx 333	. 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  1011  3anor  1106  3oran  1107  2nexaln  1833  2exanali  1864  nnel  3057  spc2d  3531  npss  4041  dfnul3OLD  4259  snprc  4650  dffv2  6845  kmlem3  9839  axpowndlem3  10286  nnunb  12159  rpnnen2lem12  15862  dsmmacl  20858  ntreq0  22136  largei  30530  ballotlem2  32355  dffr5  33627  noetasuplem4  33866  noetainflem4  33870  brsset  34118  brtxpsd  34123  dfrecs2  34179  dfint3  34181  con1bii2  35430  notbinot1  36164  elpadd0  37750  pm10.252  41868  pm10.253  41869