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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  xor3  383  imnan  400  annim  404  pm4.53  993  pm4.55  995  oran  997  nanan  1500  xnor  1520  xorneg  1530  noror  1540  alnex  1788  exnal  1834  exnalimn  1851  2exnexn  1853  nne  2939  dfrex2  3067  rexnal  3092  r2exlem  3129  ddif  4078  dfun2  4205  dfin2  4206  difin  4207  disj4  4394  snnzb  4657  eqsnuniex  5297  onuninsuci  7787  poxp2  8090  frxp3  8098  omopthi  8594  dif1enlem  9091  dfsup2  9354  rankxplim3  9803  alephgeom  10002  fin1a2lem7  10326  fin41  10364  reclem2pr  10969  ltnlei  11265  divalglem8  16367  f1omvdco3  19422  elcls  23063  ist1-2  23337  fin1aufil  23922  dchrelbas3  27226  ltsval2  27645  ltsres  27651  nosepeq  27674  nolt02o  27684  nogt01o  27685  nosupbnd2lem1  27704  noinfbnd2lem1  27719  madebdaylemlrcut  27916  oncutlt  28281  tgdim01  28600  axcontlem12  29069  avril1  30558  n0nsnel  32610  creq0  32835  axregs  35327  onvf1odlem1  35338  dftr6  35986  dfon3  36125  dffun10  36147  brub  36189  bj-bixor  36909  bj-modal4e  37067  con2bii2  37702  heiborlem1  38185  heiborlem6  38190  heiborlem8  38192  cdleme0nex  40789  aks4d1p7  42575  wopprc  43482  n0nsn2el  47495  1nevenALTV  48189  resinsnALT  49370