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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xor  1032  3anor  1125  3oran  1126  2nexaln  1863  2exanali  1893  nnel  3075  spc2d  3560  npss  4044  snprc  4678  dffv2  7006  kmlem3  10261  axpowndlem3  10714  nnunb  12632  rpnnen2lem12  16425  dsmmacl  22080  ntreq0  23428  noetasuplem4  28126  noetainflem4  28130  largei  32902  ballotlem2  35204  rankscottu  35852  dffr5  36710  brsset  36842  brtxpsd  36847  dfrecs2  36905  dfint3  36907  con1bii2  38460  notbinot1  39216  elpadd0  41069  pm10.252  45548  pm10.253  45549  ralfal  46391