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  2929  dfrex2  3056  rexnal  3082  r2exlem  3122  ddif  4104  dfun2  4233  dfin2  4234  difin  4235  disj4  4422  snnzb  4682  eqsnuniex  5316  onuninsuci  7816  poxp2  8122  frxp3  8130  omopthi  8625  dif1enlem  9120  dif1enlemOLD  9121  dfsup2  9395  rankxplim3  9834  alephgeom  10035  fin1a2lem7  10359  fin41  10397  reclem2pr  11001  ltnlei  11295  divalglem8  16370  f1omvdco3  19379  elcls  22960  ist1-2  23234  fin1aufil  23819  dchrelbas3  27149  sltval2  27568  sltres  27574  nosepeq  27597  nolt02o  27607  nogt01o  27608  nosupbnd2lem1  27627  noinfbnd2lem1  27642  madebdaylemlrcut  27810  onscutlt  28165  tgdim01  28434  axcontlem12  28902  avril1  30392  n0nsnel  32444  creq0  32659  onvf1odlem1  35090  dftr6  35738  dfon3  35880  dffun10  35902  brub  35942  bj-bixor  36579  bj-modal4e  36703  con2bii2  37321  heiborlem1  37805  heiborlem6  37810  heiborlem8  37812  cdleme0nex  40284  aks4d1p7  42071  wopprc  43019  n0nsn2el  47026  1nevenALTV  47692  resinsnALT  48861