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  2937  dfrex2  3065  rexnal  3090  r2exlem  3127  ddif  4082  dfun2  4211  dfin2  4212  difin  4213  disj4  4400  snnzb  4663  eqsnuniex  5298  onuninsuci  7784  poxp2  8086  frxp3  8094  omopthi  8590  dif1enlem  9087  dfsup2  9350  rankxplim3  9796  alephgeom  9995  fin1a2lem7  10319  fin41  10357  reclem2pr  10962  ltnlei  11258  divalglem8  16360  f1omvdco3  19415  elcls  23048  ist1-2  23322  fin1aufil  23907  dchrelbas3  27215  ltsval2  27634  ltsres  27640  nosepeq  27663  nolt02o  27673  nogt01o  27674  nosupbnd2lem1  27693  noinfbnd2lem1  27708  madebdaylemlrcut  27905  oncutlt  28270  tgdim01  28589  axcontlem12  29058  avril1  30548  n0nsnel  32600  creq0  32824  axregs  35299  onvf1odlem1  35301  dftr6  35949  dfon3  36088  dffun10  36110  brub  36152  bj-bixor  36872  bj-modal4e  37030  con2bii2  37663  heiborlem1  38146  heiborlem6  38151  heiborlem8  38153  cdleme0nex  40750  aks4d1p7  42536  wopprc  43476  n0nsn2el  47485  1nevenALTV  48179  resinsnALT  49360