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  3043  spc2d  3553  npss  4062  snprc  4671  dffv2  6925  kmlem3  10053  axpowndlem3  10499  nnunb  12386  rpnnen2lem12  16138  dsmmacl  21682  ntreq0  22995  noetasuplem4  27678  noetainflem4  27682  largei  32251  ballotlem2  34525  dffr5  35821  brsset  35954  brtxpsd  35959  dfrecs2  36017  dfint3  36019  con1bii2  37399  notbinot1  38142  elpadd0  39931  pm10.252  44481  pm10.253  44482  ralfal  45285