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 315	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2		con1bii.1	. . 3 ⊢ (¬ 𝜑 ↔ 𝜓)
3	1, 2	xchbinx 334	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
4	3	bicomi 224	1 ⊢ (¬ 𝜓 ↔ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  xor  1016  3anor  1107  3oran  1108  2nexaln  1831  2exanali  1861  nnel  3046  spc2d  3556  npss  4065  snprc  4674  dffv2  6929  kmlem3  10063  axpowndlem3  10510  nnunb  12397  rpnnen2lem12  16150  dsmmacl  21696  ntreq0  23021  noetasuplem4  27704  noetainflem4  27708  largei  32342  ballotlem2  34646  dffr5  35948  brsset  36081  brtxpsd  36086  dfrecs2  36144  dfint3  36146  con1bii2  37537  notbinot1  38280  elpadd0  40069  pm10.252  44602  pm10.253  44603  ralfal  45405