Theorem con2bii 359

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  xor3  384  imnan  403  annim  407  pm4.53  998  pm4.55  1000  oran  1002  nanan  1512  xnor  1532  xorneg  1542  noror  1552  alnex  1800  exnal  1846  exnalimn  1863  2exnexn  1865  nne  2960  dfrex2  3088  rexnal  3113  r2exlem  3150  ddif  4092  dfun2  4220  dfin2  4221  difin  4222  disj4  4410  snnzb  4674  eqsnuniex  5315  onuninsuci  7814  poxp2  8116  frxp3  8124  omopthi  8624  dif1enlem  9121  dfsup2  9383  rankxplim3  9832  alephgeom  10031  fin1a2lem7  10356  fin41  10394  reclem2pr  10999  ltnlei  11297  divalglem8  16424  f1omvdco3  19479  elcls  23120  ist1-2  23394  fin1aufil  23979  dchrelbas3  27289  ltsval2  27707  ltsres  27713  nosepeq  27736  nolt02o  27746  nogt01o  27747  nosupbnd2lem1  27766  noinfbnd2lem1  27781  madebdaylemlrcut  27979  oncutlt  28344  tgdim01  28663  axcontlem12  29132  avril1  30621  n0nsnel  32673  creq0  32898  axregs  35395  onvf1odlem1  35406  dftr6  36061  dfon3  36200  dffun10  36222  brub  36264  bj-bixor  36994  bj-modal4e  37152  con2bii2  37787  heiborlem1  38270  heiborlem6  38275  heiborlem8  38277  cdleme0nex  40874  aks4d1p7  42660  wopprc  43567  n0nsn2el  47579  1nevenALTV  48273  resinsnALT  49454