Theorem con1bii 321

Description: A contraposition inference. (Contributed by NM, 5-Aug-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		notnot 282	. . 3 ⊢ (φ ↔ ¬ ¬ φ)
2		con1bii.1	. . 3 ⊢ (¬ φ ↔ ψ)
3	1, 2	xchbinx 301	. 2 ⊢ (φ ↔ ¬ ψ)
4	3	bicomi 193	1 ⊢ (¬ ψ ↔ φ)

Syntax hints:  ¬ wn 3   ↔ wb 176

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 177

This theorem is referenced by:  con2bii  322  xor  861  3oran  951  had0  1403  mpto2OLD  1535  necon1abii  2568  necon1bbii  2569  npss  3380  dfnul3  3554  disj  3592  snprc  3789  dfpss4  3889  0nel1c  4160  dfnnc2  4396  eqpw1relk  4480  eqtfinrelk  4487  releqel  5808  fnfullfunlem1  5857  ovcelem1  6172  tcfnex  6245  nclennlem1  6249  nnc3n3p1  6279  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305  fnfreclem1  6318