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  3081  r2exlem  3118  ddif  4094  dfun2  4223  dfin2  4224  difin  4225  disj4  4412  snnzb  4672  eqsnuniex  5303  onuninsuci  7780  poxp2  8083  frxp3  8091  omopthi  8586  dif1enlem  9080  dif1enlemOLD  9081  dfsup2  9353  rankxplim3  9796  alephgeom  9995  fin1a2lem7  10319  fin41  10357  reclem2pr  10961  ltnlei  11255  divalglem8  16329  f1omvdco3  19346  elcls  22976  ist1-2  23250  fin1aufil  23835  dchrelbas3  27165  sltval2  27584  sltres  27590  nosepeq  27613  nolt02o  27623  nogt01o  27624  nosupbnd2lem1  27643  noinfbnd2lem1  27658  madebdaylemlrcut  27831  onscutlt  28188  tgdim01  28470  axcontlem12  28938  avril1  30425  n0nsnel  32477  creq0  32692  axregs  35073  onvf1odlem1  35075  dftr6  35723  dfon3  35865  dffun10  35887  brub  35927  bj-bixor  36564  bj-modal4e  36688  con2bii2  37306  heiborlem1  37790  heiborlem6  37795  heiborlem8  37797  cdleme0nex  40269  aks4d1p7  42056  wopprc  43003  n0nsn2el  47010  1nevenALTV  47676  resinsnALT  48858