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  988  pm4.55  990  oran  992  nanan  1495  xnor  1515  xorneg  1525  noror  1535  alnex  1783  exnal  1829  exnalimn  1846  2exnexn  1848  nne  2937  dfrex2  3065  rexnal  3090  r2exlem  3127  ddif  4095  dfun2  4224  dfin2  4225  difin  4226  disj4  4413  snnzb  4677  eqsnuniex  5308  onuninsuci  7792  poxp2  8095  frxp3  8103  omopthi  8599  dif1enlem  9096  dfsup2  9359  rankxplim3  9805  alephgeom  10004  fin1a2lem7  10328  fin41  10366  reclem2pr  10971  ltnlei  11266  divalglem8  16339  f1omvdco3  19390  elcls  23029  ist1-2  23303  fin1aufil  23888  dchrelbas3  27217  ltsval2  27636  ltsres  27642  nosepeq  27665  nolt02o  27675  nogt01o  27676  nosupbnd2lem1  27695  noinfbnd2lem1  27710  madebdaylemlrcut  27907  oncutlt  28272  tgdim01  28591  axcontlem12  29060  avril1  30550  n0nsnel  32601  creq0  32825  axregs  35314  onvf1odlem1  35316  dftr6  35964  dfon3  36103  dffun10  36125  brub  36167  bj-bixor  36813  bj-modal4e  36957  con2bii2  37585  heiborlem1  38059  heiborlem6  38064  heiborlem8  38066  cdleme0nex  40663  aks4d1p7  42450  wopprc  43384  n0nsn2el  47382  1nevenALTV  48048  resinsnALT  49229