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  1493  xnor  1513  xorneg  1523  noror  1533  alnex  1781  exnal  1827  exnalimn  1844  2exnexn  1846  nne  2930  dfrex2  3057  rexnal  3083  r2exlem  3123  ddif  4107  dfun2  4236  dfin2  4237  difin  4238  disj4  4425  snnzb  4685  eqsnuniex  5319  onuninsuci  7819  poxp2  8125  frxp3  8133  omopthi  8628  dif1enlem  9126  dif1enlemOLD  9127  dfsup2  9402  rankxplim3  9841  alephgeom  10042  fin1a2lem7  10366  fin41  10404  reclem2pr  11008  ltnlei  11302  divalglem8  16377  f1omvdco3  19386  elcls  22967  ist1-2  23241  fin1aufil  23826  dchrelbas3  27156  sltval2  27575  sltres  27581  nosepeq  27604  nolt02o  27614  nogt01o  27615  nosupbnd2lem1  27634  noinfbnd2lem1  27649  madebdaylemlrcut  27817  onscutlt  28172  tgdim01  28441  axcontlem12  28909  avril1  30399  n0nsnel  32451  creq0  32666  onvf1odlem1  35097  dftr6  35745  dfon3  35887  dffun10  35909  brub  35949  bj-bixor  36586  bj-modal4e  36710  con2bii2  37328  heiborlem1  37812  heiborlem6  37817  heiborlem8  37819  cdleme0nex  40291  aks4d1p7  42078  wopprc  43026  n0nsn2el  47030  1nevenALTV  47696  resinsnALT  48865