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  988  pm4.55  990  oran  992  nanan  1495  xnor  1515  xorneg  1525  noror  1535  alnex  1783  exnal  1829  exnalimn  1846  2exnexn  1848  nne  2936  dfrex2  3064  rexnal  3089  r2exlem  3126  ddif  4081  dfun2  4210  dfin2  4211  difin  4212  disj4  4399  snnzb  4662  eqsnuniex  5303  onuninsuci  7791  poxp2  8093  frxp3  8101  omopthi  8597  dif1enlem  9094  dfsup2  9357  rankxplim3  9805  alephgeom  10004  fin1a2lem7  10328  fin41  10366  reclem2pr  10971  ltnlei  11267  divalglem8  16369  f1omvdco3  19424  elcls  23038  ist1-2  23312  fin1aufil  23897  dchrelbas3  27201  ltsval2  27620  ltsres  27626  nosepeq  27649  nolt02o  27659  nogt01o  27660  nosupbnd2lem1  27679  noinfbnd2lem1  27694  madebdaylemlrcut  27891  oncutlt  28256  tgdim01  28575  axcontlem12  29044  avril1  30533  n0nsnel  32585  creq0  32809  axregs  35283  onvf1odlem1  35285  dftr6  35933  dfon3  36072  dffun10  36094  brub  36136  bj-bixor  36856  bj-modal4e  37014  con2bii2  37649  heiborlem1  38132  heiborlem6  38137  heiborlem8  38139  cdleme0nex  40736  aks4d1p7  42522  wopprc  43458  n0nsn2el  47473  1nevenALTV  48167  resinsnALT  49348