Theorem con1bii 346

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

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  con2bii  347  xor  934  3oran  1055  2nexaln  1754  nnel  2902  npss  3695  symdifass  3831  dfnul3  3894  snprc  4223  dffv2  6228  kmlem3  8918  axpowndlem3  9365  nnunb  11232  rpnnen2lem12  14879  dsmmacl  20004  ntreq0  20791  largei  28972  spc2d  29159  ballotlem2  30328  dffr5  31348  brsset  31635  brtxpsd  31640  dfrecs2  31696  dfint3  31698  con1bii2  32808  notbinot1  33507  elpadd0  34572  pm10.252  38039  pm10.253  38040  2exanali  38066