Theorem con1bii 357

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  xor  1022  3anor  1113  3oran  1114  2nexaln  1837  2exanali  1867  nnel  3049  spc2d  3547  npss  4051  snprc  4656  dffv2  6929  kmlem3  10073  axpowndlem3  10520  nnunb  12431  rpnnen2lem12  16190  dsmmacl  21723  ntreq0  23067  noetasuplem4  27725  noetainflem4  27729  largei  32363  ballotlem2  34680  dffr5  35989  brsset  36122  brtxpsd  36127  dfrecs2  36185  dfint3  36187  con1bii2  37701  notbinot1  38453  elpadd0  40308  pm10.252  44812  pm10.253  44813  ralfal  45615