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  2936  dfrex2  3063  rexnal  3089  r2exlem  3129  ddif  4116  dfun2  4245  dfin2  4246  difin  4247  disj4  4434  snnzb  4694  eqsnuniex  5331  onuninsuci  7835  poxp2  8142  frxp3  8150  omopthi  8673  dif1enlem  9170  dif1enlemOLD  9171  dfsup2  9456  rankxplim3  9895  alephgeom  10096  fin1a2lem7  10420  fin41  10458  reclem2pr  11062  1re  11235  ltnlei  11356  divalglem8  16419  f1omvdco3  19430  elcls  23011  ist1-2  23285  fin1aufil  23870  dchrelbas3  27201  sltval2  27620  sltres  27626  nosepeq  27649  nolt02o  27659  nogt01o  27660  nosupbnd2lem1  27679  noinfbnd2lem1  27694  madebdaylemlrcut  27862  onscutlt  28217  tgdim01  28486  axcontlem12  28954  avril1  30444  n0nsnel  32496  creq0  32713  dftr6  35768  dfon3  35910  dffun10  35932  brub  35972  bj-bixor  36609  bj-modal4e  36733  con2bii2  37351  heiborlem1  37835  heiborlem6  37840  heiborlem8  37842  cdleme0nex  40309  aks4d1p7  42096  wopprc  43054  n0nsn2el  47054  1nevenALTV  47705  resinsnALT  48848