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  1494  xnor  1514  xorneg  1524  noror  1534  alnex  1782  exnal  1828  exnalimn  1845  2exnexn  1847  nne  2936  dfrex2  3063  rexnal  3088  r2exlem  3125  ddif  4093  dfun2  4222  dfin2  4223  difin  4224  disj4  4411  snnzb  4675  eqsnuniex  5306  onuninsuci  7782  poxp2  8085  frxp3  8093  omopthi  8589  dif1enlem  9084  dfsup2  9347  rankxplim3  9793  alephgeom  9992  fin1a2lem7  10316  fin41  10354  reclem2pr  10959  ltnlei  11254  divalglem8  16327  f1omvdco3  19378  elcls  23017  ist1-2  23291  fin1aufil  23876  dchrelbas3  27205  ltsval2  27624  ltsres  27630  nosepeq  27653  nolt02o  27663  nogt01o  27664  nosupbnd2lem1  27683  noinfbnd2lem1  27698  madebdaylemlrcut  27895  oncutlt  28260  tgdim01  28579  axcontlem12  29048  avril1  30538  n0nsnel  32590  creq0  32815  axregs  35295  onvf1odlem1  35297  dftr6  35945  dfon3  36084  dffun10  36106  brub  36148  bj-bixor  36791  bj-modal4e  36916  con2bii2  37538  heiborlem1  38012  heiborlem6  38017  heiborlem8  38019  cdleme0nex  40550  aks4d1p7  42337  wopprc  43272  n0nsn2el  47271  1nevenALTV  47937  resinsnALT  49118