Theorem con1bii 356

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 224	1 ⊢ (¬ 𝜓 ↔ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  xor  1017  3anor  1108  3oran  1109  2nexaln  1830  2exanali  1860  nnel  3056  spc2d  3602  npss  4113  snprc  4717  dffv2  7004  kmlem3  10193  axpowndlem3  10639  nnunb  12522  rpnnen2lem12  16261  dsmmacl  21761  ntreq0  23085  noetasuplem4  27781  noetainflem4  27785  largei  32286  ballotlem2  34491  dffr5  35754  brsset  35890  brtxpsd  35895  dfrecs2  35951  dfint3  35953  con1bii2  37333  notbinot1  38086  elpadd0  39811  pm10.252  44380  pm10.253  44381  ralfal  45166