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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  xor3  385  imnan  404  annim  408  pm4.53  1001  pm4.55  1003  oran  1005  nanan  1516  xnor  1536  xorneg  1546  noror  1556  alnex  1804  exnal  1850  exnalimn  1867  2exnexn  1869  nne  2964  dfrex2  3092  rexnal  3117  r2exlem  3154  ddif  4097  dfun2  4225  dfin2  4226  difin  4227  disj4  4416  snnzb  4680  eqsnuniex  5322  onuninsuci  7824  poxp2  8127  frxp3  8135  omopthi  8635  dif1enlem  9132  dfsup2  9392  rankxplim3  9841  alephgeom  10054  fin1a2lem7  10378  fin41  10416  reclem2pr  11021  ltnlei  11319  divalglem8  16446  f1omvdco3  19507  elcls  23187  ist1-2  23461  fin1aufil  24046  dchrelbas3  27356  ltsval2  27774  ltsres  27780  nosepeq  27803  nolt02o  27813  nogt01o  27814  nosupbnd2lem1  27833  noinfbnd2lem1  27848  madebdaylemlrcut  28046  oncutlt  28411  tgdim01  28730  axcontlem12  29230  avril1  30719  n0nsnel  32767  creq0  32989  axregs  35442  onvf1odlem1  35453  dftr6  36109  dfon3  36248  dffun10  36270  brub  36312  bj-bixor  37041  bj-modal4e  37199  con2bii2  37834  heiborlem1  38317  heiborlem6  38322  heiborlem8  38324  cdleme0nex  40921  aks4d1p7  42707  wopprc  43614  n0nsn2el  47618  1nevenALTV  48312  resinsnALT  49503