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  2961  dfrex2  3091  rexnal  3116  r2exlem  3153  ddif  4091  dfun2  4219  dfin2  4220  difin  4221  disj4  4415  snnzb  4682  eqsnuniex  5330  onuninsuci  7840  poxp2  8145  frxp3  8153  omopthi  8653  dif1enlem  9158  dfsup2  9418  rankxplim3  9867  alephgeom  10089  fin1a2lem7  10412  fin41  10450  reclem2pr  11061  ltnlei  11359  divalglem8  16496  f1omvdco3  19582  elcls  23304  ist1-2  23578  fin1aufil  24164  dchrelbas3  27482  ltsval2  27900  ltsres  27906  nosepeq  27929  nolt02o  27939  nogt01o  27940  nosupbnd2lem1  27959  noinfbnd2lem1  27974  madebdaylemlrcut  28172  oncutlt  28537  tgdim01  28857  axcontlem12  29440  avril1  30951  n0nsnel  32998  creq0  33215  axregs  35673  onvf1odlem1  35708  dftr6  36338  dfon3  36477  dffun10  36499  brub  36541  bj-bixor  37300  bj-modal4e  37458  con2bii2  38095  heiborlem1  38569  heiborlem6  38574  heiborlem8  38576  cdleme0nex  41171  aks4d1p7  42957  wopprc  43879  n0nsn2el  47921  1nevenALTV  48615  resinsnALT  49807