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  2567  necon1bbii  2568  npss  3379  dfnul3  3553  disj  3591  snprc  3788  dfpss4  3888  0nel1c  4159  dfnnc2  4395  eqpw1relk  4479  eqtfinrelk  4486  releqel  5807  fnfullfunlem1  5856  ovcelem1  6171  tcfnex  6244  nclennlem1  6248  nnc3n3p1  6278  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304  fnfreclem1  6317