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  1494  xnor  1514  xorneg  1524  noror  1534  alnex  1782  exnal  1828  exnalimn  1845  2exnexn  1847  nne  2932  dfrex2  3059  rexnal  3084  r2exlem  3121  ddif  4091  dfun2  4220  dfin2  4221  difin  4222  disj4  4409  snnzb  4671  eqsnuniex  5299  onuninsuci  7770  poxp2  8073  frxp3  8081  omopthi  8576  dif1enlem  9069  dfsup2  9328  rankxplim3  9774  alephgeom  9973  fin1a2lem7  10297  fin41  10335  reclem2pr  10939  ltnlei  11234  divalglem8  16311  f1omvdco3  19362  elcls  22989  ist1-2  23263  fin1aufil  23848  dchrelbas3  27177  sltval2  27596  sltres  27602  nosepeq  27625  nolt02o  27635  nogt01o  27636  nosupbnd2lem1  27655  noinfbnd2lem1  27670  madebdaylemlrcut  27845  onscutlt  28202  tgdim01  28486  axcontlem12  28954  avril1  30441  n0nsnel  32493  creq0  32717  axregs  35143  onvf1odlem1  35145  dftr6  35793  dfon3  35932  dffun10  35954  brub  35994  bj-bixor  36631  bj-modal4e  36755  con2bii2  37373  heiborlem1  37857  heiborlem6  37862  heiborlem8  37864  cdleme0nex  40335  aks4d1p7  42122  wopprc  43069  n0nsn2el  47062  1nevenALTV  47728  resinsnALT  48910