Theorem con2bii 357

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 206

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 207

This theorem is referenced by:  xor3  382  imnan  399  annim  403  pm4.53  986  pm4.55  988  oran  990  nanan  1490  xnor  1510  xorneg  1520  noror  1530  alnex  1779  exnal  1825  exnalimn  1842  2exnexn  1844  nne  2950  dfrex2  3079  rexnal  3106  r2exlem  3149  ddif  4164  dfun2  4289  dfin2  4290  difin  4291  disj4  4482  snnzb  4743  eqsnuniex  5379  onuninsuci  7877  poxp2  8184  frxp3  8192  omopthi  8717  dif1enlem  9222  dif1enlemOLD  9223  dfsup2  9513  rankxplim3  9950  alephgeom  10151  fin1a2lem7  10475  fin41  10513  reclem2pr  11117  1re  11290  ltnlei  11411  divalglem8  16448  f1omvdco3  19491  elcls  23102  ist1-2  23376  fin1aufil  23961  dchrelbas3  27300  sltval2  27719  sltres  27725  nosepeq  27748  nolt02o  27758  nogt01o  27759  nosupbnd2lem1  27778  noinfbnd2lem1  27793  madebdaylemlrcut  27955  tgdim01  28533  axcontlem12  29008  avril1  30495  n0nsnel  32544  creq0  32749  dftr6  35713  dfon3  35856  dffun10  35878  brub  35918  bj-bixor  36557  bj-modal4e  36681  con2bii2  37299  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  cdleme0nex  40247  aks4d1p7  42040  wopprc  42987  n0nsn2el  46940  1nevenALTV  47565