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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xor3  385  imnan  405  annim  409  pm4.53  1001  pm4.55  1003  oran  1005  nanan  1523  xnor  1543  xorneg  1553  noror  1563  alnex  1814  exnal  1860  exnalimn  1877  2exnexn  1879  nne  2965  dfrex2  3095  rexnal  3120  r2exlem  3157  ddif  4098  dfun2  4226  dfin2  4227  difin  4228  disj4  4422  snnzb  4689  eqsnuniex  5337  onuninsuci  7845  poxp2  8148  frxp3  8156  omopthi  8656  dif1enlem  9154  dfsup2  9414  rankxplim3  9863  alephgeom  10085  fin1a2lem7  10408  fin41  10446  reclem2pr  11051  ltnlei  11349  divalglem8  16483  f1omvdco3  19550  elcls  23267  ist1-2  23541  fin1aufil  24126  dchrelbas3  27439  ltsval2  27857  ltsres  27863  nosepeq  27886  nolt02o  27896  nogt01o  27897  nosupbnd2lem1  27916  noinfbnd2lem1  27931  madebdaylemlrcut  28129  oncutlt  28494  tgdim01  28813  axcontlem12  29362  avril1  30851  n0nsnel  32898  creq0  33118  axregs  35576  onvf1odlem1  35611  dftr6  36264  dfon3  36403  dffun10  36425  brub  36467  bj-bixor  37225  bj-modal4e  37383  con2bii2  38020  heiborlem1  38503  heiborlem6  38508  heiborlem8  38510  cdleme0nex  41105  aks4d1p7  42891  wopprc  43798  n0nsn2el  47803  1nevenALTV  48497  resinsnALT  49692