Theorem con2bii 360

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xor3  385  imnan  405  annim  409  pm4.53  1001  pm4.55  1003  oran  1005  nanan  1522  xnor  1542  xorneg  1552  noror  1562  alnex  1813  exnal  1859  exnalimn  1876  2exnexn  1878  nne  2959  dfrex2  3089  rexnal  3114  r2exlem  3151  ddif  4077  dfun2  4215  dfin2  4216  difin  4217  disj4  4411  snnzb  4675  eqsnuniex  5322  onuninsuci  7852  poxp2  8163  frxp3  8171  omopthi  8674  dif1enlem  9179  dfsup2  9440  rankxplim3  9902  alephgeom  10165  fin1a2lem7  10488  fin41  10526  reclem2pr  11137  ltnlei  11435  divalglem8  16576  f1omvdco3  19669  elcls  23397  ist1-2  23671  fin1aufil  24257  dchrelbas3  27571  ltsval2  28019  ltsres  28025  nosepeq  28048  nolt02o  28058  nogt01o  28059  nosupbnd2lem1  28078  noinfbnd2lem1  28093  madebdaylemlrcut  28291  oncutlt  28656  tgdim01  28976  axcontlem12  29559  avril1  31070  n0nsnel  33159  creq0  33375  axregs  35864  j0ltaleph  35948  onvf1odlem1  35951  dftr6  36609  dfon3  36747  dffun10  36769  brub  36811  bj-bixor  37554  bj-modal4e  37712  con2bii2  38350  heiborlem1  38839  heiborlem6  38844  heiborlem8  38846  cdleme0nex  41441  aks4d1p7  43227  wopprc  44131  n0nsn2el  48189  1nevenALTV  48883  resinsnALT  50080