Theorem con2bii 356

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 314	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 334	1 ⊢ (𝜓 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xor3  381  imnan  398  annim  402  pm4.53  982  pm4.55  984  oran  986  nanan  1489  xnor  1509  xorneg  1520  noror  1532  alnex  1781  exnal  1827  exnalimn  1844  2exnexn  1846  nne  2942  dfrex2  3071  rexnal  3098  r2exlem  3141  ddif  4135  dfun2  4258  dfin2  4259  difin  4260  disj4  4457  snnzb  4721  eqsnuniex  5358  onuninsuci  7831  poxp2  8131  frxp3  8139  omopthi  8662  dif1enlem  9158  dif1enlemOLD  9159  dfsup2  9441  rankxplim3  9878  alephgeom  10079  fin1a2lem7  10403  fin41  10441  reclem2pr  11045  1re  11218  ltnlei  11339  divalglem8  16347  f1omvdco3  19358  elcls  22797  ist1-2  23071  fin1aufil  23656  dchrelbas3  26977  sltval2  27395  sltres  27401  nosepeq  27424  nolt02o  27434  nogt01o  27435  nosupbnd2lem1  27454  noinfbnd2lem1  27469  madebdaylemlrcut  27630  tgdim01  28025  axcontlem12  28500  avril1  29983  creq0  32227  dftr6  35025  dfon3  35168  dffun10  35190  brub  35230  bj-bixor  35772  bj-modal4e  35896  con2bii2  36517  heiborlem1  36982  heiborlem6  36987  heiborlem8  36989  cdleme0nex  39464  aks4d1p7  41254  wopprc  42071  n0nsn2el  46033  1nevenALTV  46657