Theorem con2bii 358

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 205

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 206

This theorem is referenced by:  xor3  384  imnan  401  annim  405  pm4.53  984  pm4.55  986  oran  988  nanan  1491  xnor  1511  xorneg  1522  noror  1534  alnex  1783  exnal  1829  exnalimn  1846  2exnexn  1848  nne  2945  dfrex2  3074  rexnal  3100  r2exlem  3137  ddif  4088  dfun2  4211  dfin2  4212  difin  4213  disj4  4410  snnzb  4671  eqsnuniex  5308  onuninsuci  7759  omopthi  8567  dif1enlem  9026  dif1enlemOLD  9027  dfsup2  9306  rankxplim3  9743  alephgeom  9944  fin1a2lem7  10268  fin41  10306  reclem2pr  10910  1re  11081  ltnlei  11202  divalglem8  16209  f1omvdco3  19154  elcls  22330  ist1-2  22604  fin1aufil  23189  dchrelbas3  26492  sltval2  26910  sltres  26916  nosepeq  26939  nolt02o  26949  nogt01o  26950  nosupbnd2lem1  26969  noinfbnd2lem1  26984  tgdim01  27157  axcontlem12  27632  avril1  29115  creq0  31355  dftr6  34007  poxp2  34072  poxp3  34078  frxp3  34079  madebdaylemlrcut  34187  dfon3  34331  dffun10  34353  brub  34393  bj-bixor  34910  bj-modal4e  35034  con2bii2  35658  heiborlem1  36123  heiborlem6  36128  heiborlem8  36130  cdleme0nex  38607  aks4d1p7  40394  wopprc  41164  1nevenALTV  45559