Theorem con2bii 360

Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.)

Hypothesis

Ref	Expression
con2bii.1	⊢ (𝜑 ↔ ¬ 𝜓)

Assertion

Ref	Expression
con2bii	⊢ (𝜓 ↔ ¬ 𝜑)

Proof of Theorem con2bii

Step	Hyp	Ref	Expression
1		notnotb 317	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 337	1 ⊢ (𝜓 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  xor3  386  imnan  402  annim  406  pm4.53  982  pm4.55  984  oran  986  nanan  1483  xnor  1503  xorneg  1514  noror  1528  alnex  1782  exnal  1827  exnalimn  1844  2exnexn  1846  equs3OLD  1965  19.3vOLD  1989  nne  3020  rexnal  3238  dfrex2  3239  r2exlem  3302  ddif  4113  dfun2  4236  dfin2  4237  difin  4238  dfnul2OLD  4294  disj4  4408  snnzb  4654  onuninsuci  7555  omopthi  8284  dfsup2  8908  rankxplim3  9310  alephgeom  9508  fin1a2lem7  9828  fin41  9866  reclem2pr  10470  1re  10641  ltnlei  10761  divalglem8  15751  f1omvdco3  18577  elcls  21681  ist1-2  21955  fin1aufil  22540  dchrelbas3  25814  tgdim01  26293  axcontlem12  26761  avril1  28242  creq0  30471  dftr6  32986  sltval2  33163  sltres  33169  nosepeq  33189  nolt02o  33199  nosupbnd2lem1  33215  dfon3  33353  dffun10  33375  brub  33415  bj-bixor  33925  bj-modal4e  34049  con2bii2  34617  wl-dfrexex  34865  wl-dfrexsb  34866  heiborlem1  35104  heiborlem6  35109  heiborlem8  35111  cdleme0nex  37441  wopprc  39647  1nevenALTV  43876