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  2933  dfrex2  3060  rexnal  3085  r2exlem  3122  ddif  4090  dfun2  4219  dfin2  4220  difin  4221  disj4  4408  snnzb  4672  eqsnuniex  5303  onuninsuci  7778  poxp2  8081  frxp3  8089  omopthi  8584  dif1enlem  9078  dfsup2  9337  rankxplim3  9783  alephgeom  9982  fin1a2lem7  10306  fin41  10344  reclem2pr  10948  ltnlei  11243  divalglem8  16315  f1omvdco3  19365  elcls  22991  ist1-2  23265  fin1aufil  23850  dchrelbas3  27179  sltval2  27598  sltres  27604  nosepeq  27627  nolt02o  27637  nogt01o  27638  nosupbnd2lem1  27657  noinfbnd2lem1  27672  madebdaylemlrcut  27847  onscutlt  28204  tgdim01  28488  axcontlem12  28957  avril1  30447  n0nsnel  32499  creq0  32725  axregs  35168  onvf1odlem1  35170  dftr6  35818  dfon3  35957  dffun10  35979  brub  36021  bj-bixor  36658  bj-modal4e  36782  con2bii2  37400  heiborlem1  37874  heiborlem6  37879  heiborlem8  37881  cdleme0nex  40412  aks4d1p7  42199  wopprc  43150  n0nsn2el  47152  1nevenALTV  47818  resinsnALT  49000