Theorem con2bii 357

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 315	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 335	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:  xor3  382  imnan  399  annim  403  pm4.53  987  pm4.55  989  oran  991  nanan  1490  xnor  1510  xorneg  1520  noror  1530  alnex  1778  exnal  1824  exnalimn  1841  2exnexn  1843  nne  2942  dfrex2  3071  rexnal  3098  r2exlem  3141  ddif  4151  dfun2  4276  dfin2  4277  difin  4278  disj4  4465  snnzb  4723  eqsnuniex  5367  onuninsuci  7861  poxp2  8167  frxp3  8175  omopthi  8698  dif1enlem  9195  dif1enlemOLD  9196  dfsup2  9482  rankxplim3  9919  alephgeom  10120  fin1a2lem7  10444  fin41  10482  reclem2pr  11086  1re  11259  ltnlei  11380  divalglem8  16434  f1omvdco3  19482  elcls  23097  ist1-2  23371  fin1aufil  23956  dchrelbas3  27297  sltval2  27716  sltres  27722  nosepeq  27745  nolt02o  27755  nogt01o  27756  nosupbnd2lem1  27775  noinfbnd2lem1  27790  madebdaylemlrcut  27952  tgdim01  28530  axcontlem12  29005  avril1  30492  n0nsnel  32543  creq0  32753  dftr6  35731  dfon3  35874  dffun10  35896  brub  35936  bj-bixor  36574  bj-modal4e  36698  con2bii2  37316  heiborlem1  37798  heiborlem6  37803  heiborlem8  37805  cdleme0nex  40273  aks4d1p7  42065  wopprc  43019  n0nsn2el  46975  1nevenALTV  47616