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 317	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 337	1 ⊢ (𝜓 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  xor3  386  imnan  402  annim  406  pm4.53  982  pm4.55  984  oran  986  nanan  1480  xnor  1500  xorneg  1510  noror  1522  alnex  1776  exnal  1821  exnalimn  1838  2exnexn  1840  equs3OLD  1959  19.3vOLD  1983  nne  3018  rexnal  3236  dfrex2  3237  r2exlem  3300  ddif  4111  dfun2  4234  dfin2  4235  difin  4236  dfnul2OLD  4292  disj4  4406  snnzb  4646  onuninsuci  7547  omopthi  8276  dfsup2  8900  rankxplim3  9302  alephgeom  9500  fin1a2lem7  9820  fin41  9858  reclem2pr  10462  1re  10633  ltnlei  10753  divalglem8  15743  f1omvdco3  18569  elcls  21673  ist1-2  21947  fin1aufil  22532  dchrelbas3  25806  tgdim01  26285  axcontlem12  26753  avril1  28234  creq0  30463  dftr6  32979  sltval2  33156  sltres  33162  nosepeq  33182  nolt02o  33192  nosupbnd2lem1  33208  dfon3  33346  dffun10  33368  brub  33408  bj-bixor  33918  bj-modal4e  34042  con2bii2  34606  wl-dfrexex  34842  wl-dfrexsb  34843  heiborlem1  35081  heiborlem6  35086  heiborlem8  35088  cdleme0nex  37418  wopprc  39617  1nevenALTV  43846