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  1493  xnor  1513  xorneg  1523  noror  1533  alnex  1781  exnal  1827  exnalimn  1844  2exnexn  1846  nne  2944  dfrex2  3073  rexnal  3100  r2exlem  3143  ddif  4141  dfun2  4270  dfin2  4271  difin  4272  disj4  4459  snnzb  4718  eqsnuniex  5361  onuninsuci  7861  poxp2  8168  frxp3  8176  omopthi  8699  dif1enlem  9196  dif1enlemOLD  9197  dfsup2  9484  rankxplim3  9921  alephgeom  10122  fin1a2lem7  10446  fin41  10484  reclem2pr  11088  1re  11261  ltnlei  11382  divalglem8  16437  f1omvdco3  19467  elcls  23081  ist1-2  23355  fin1aufil  23940  dchrelbas3  27282  sltval2  27701  sltres  27707  nosepeq  27730  nolt02o  27740  nogt01o  27741  nosupbnd2lem1  27760  noinfbnd2lem1  27775  madebdaylemlrcut  27937  tgdim01  28515  axcontlem12  28990  avril1  30482  n0nsnel  32534  creq0  32746  dftr6  35751  dfon3  35893  dffun10  35915  brub  35955  bj-bixor  36592  bj-modal4e  36716  con2bii2  37334  heiborlem1  37818  heiborlem6  37823  heiborlem8  37825  cdleme0nex  40292  aks4d1p7  42084  wopprc  43042  n0nsn2el  47037  1nevenALTV  47678  resinsnALT  48773