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  3042  spc2d  3557  npss  4063  snprc  4670  dffv2  6917  kmlem3  10044  axpowndlem3  10490  nnunb  12377  rpnnen2lem12  16134  dsmmacl  21679  ntreq0  22993  noetasuplem4  27676  noetainflem4  27680  largei  32245  ballotlem2  34500  dffr5  35796  brsset  35929  brtxpsd  35934  dfrecs2  35990  dfint3  35992  con1bii2  37372  notbinot1  38125  elpadd0  39854  pm10.252  44400  pm10.253  44401  ralfal  45204