Theorem con2bii 361

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 ⊢ (𝜓 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  xor3  387  imnan  403  annim  407  pm4.53  983  pm4.55  985  oran  987  nanan  1484  xnor  1504  xorneg  1515  noror  1529  alnex  1783  exnal  1828  exnalimn  1845  2exnexn  1847  equs3OLD  1965  19.3vOLD  1989  nne  2991  rexnal  3201  dfrex2  3202  r2exlem  3261  ddif  4064  dfun2  4186  dfin2  4187  difin  4188  disj4  4366  snnzb  4614  onuninsuci  7535  omopthi  8267  dfsup2  8892  rankxplim3  9294  alephgeom  9493  fin1a2lem7  9817  fin41  9855  reclem2pr  10459  1re  10630  ltnlei  10750  divalglem8  15741  f1omvdco3  18569  elcls  21678  ist1-2  21952  fin1aufil  22537  dchrelbas3  25822  tgdim01  26301  axcontlem12  26769  avril1  28248  creq0  30497  dftr6  33099  sltval2  33276  sltres  33282  nosepeq  33302  nolt02o  33312  nosupbnd2lem1  33328  dfon3  33466  dffun10  33488  brub  33528  bj-bixor  34038  bj-modal4e  34162  con2bii2  34750  wl-dfrexex  35015  wl-dfrexsb  35016  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  cdleme0nex  37586  wopprc  39971  1nevenALTV  44209