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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xor  1014  3anor  1109  3oran  1110  2nexaln  1833  2exanali  1864  nnel  3057  spc2d  3593  npss  4111  dfnul3OLD  4329  snprc  4722  dffv2  6987  kmlem3  10147  axpowndlem3  10594  nnunb  12468  rpnnen2lem12  16168  dsmmacl  21296  ntreq0  22581  noetasuplem4  27239  noetainflem4  27243  largei  31520  ballotlem2  33487  dffr5  34724  brsset  34861  brtxpsd  34866  dfrecs2  34922  dfint3  34924  con1bii2  36213  notbinot1  36947  elpadd0  38680  pm10.252  43120  pm10.253  43121  ralfal  43855