Theorem con1bii 345

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

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  con2bii  346  xor  931  3oran  1050  2nexaln  1747  nnel  2892  npss  3679  symdifass  3815  dfnul3  3877  snprc  4197  dffv2  6181  kmlem3  8857  axpowndlem3  9300  nnunb  11165  rpnnen2lem12  14793  dsmmacl  19904  ntreq0  20691  largei  28510  spc2d  28697  ballotlem2  29877  dffr5  30896  brsset  31166  brtxpsd  31171  dfrecs2  31227  dfint3  31229  con1bii2  32355  notbinot1  33048  elpadd0  34113  pm10.252  37582  pm10.253  37583  2exanali  37609