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 ⊢ (¬ 𝜓 ↔ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  xor  1030  3anor  1123  3oran  1124  2nexaln  1853  2exanali  1883  nnel  3074  spc2d  3564  npss  4070  snprc  4679  dffv2  6966  kmlem3  10124  axpowndlem3  10572  nnunb  12488  rpnnen2lem12  16269  dsmmacl  21848  ntreq0  23191  noetasuplem4  27854  noetainflem4  27858  largei  32524  ballotlem2  34791  dffr5  36112  brsset  36245  brtxpsd  36250  dfrecs2  36308  dfint3  36310  con1bii2  37833  notbinot1  38585  elpadd0  40440  pm10.252  44930  pm10.253  44931  ralfal  45738