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  1523  xnor  1543  xorneg  1553  noror  1563  alnex  1814  exnal  1860  exnalimn  1877  2exnexn  1879  nne  2963  dfrex2  3093  rexnal  3118  r2exlem  3155  ddif  4080  dfun2  4218  dfin2  4219  difin  4220  disj4  4415  snnzb  4679  eqsnuniex  5328  onuninsuci  7878  poxp2  8190  frxp3  8198  omopthi  8701  dif1enlem  9206  dfsup2  9466  rankxplim3  9928  alephgeom  10191  fin1a2lem7  10514  fin41  10552  reclem2pr  11163  ltnlei  11461  divalglem8  16602  f1omvdco3  19696  elcls  23424  ist1-2  23698  fin1aufil  24284  dchrelbas3  27598  ltsval2  28046  ltsres  28052  nosepeq  28075  nolt02o  28085  nogt01o  28086  nosupbnd2lem1  28105  noinfbnd2lem1  28120  madebdaylemlrcut  28318  oncutlt  28683  tgdim01  29003  axcontlem12  29586  avril1  31097  n0nsnel  33186  creq0  33401  axregs  35920  j0ltaleph  36021  onvf1odlem1  36044  dftr6  36707  dfon3  36845  dffun10  36867  brub  36909  bj-bixor  37652  bj-modal4e  37810  con2bii2  38461  heiborlem1  38948  heiborlem6  38953  heiborlem8  38955  cdleme0nex  41550  aks4d1p7  43336  wopprc  44241  n0nsn2el  48310  1nevenALTV  49004  resinsnALT  50201