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  5310  onuninsuci  7794  poxp2  8097  frxp3  8105  omopthi  8601  dif1enlem  9098  dfsup2  9361  rankxplim3  9807  alephgeom  10006  fin1a2lem7  10330  fin41  10368  reclem2pr  10973  ltnlei  11268  divalglem8  16341  f1omvdco3  19395  elcls  23034  ist1-2  23308  fin1aufil  23893  dchrelbas3  27222  ltsval2  27641  ltsres  27647  nosepeq  27670  nolt02o  27680  nogt01o  27681  nosupbnd2lem1  27700  noinfbnd2lem1  27715  madebdaylemlrcut  27912  oncutlt  28277  tgdim01  28597  axcontlem12  29066  avril1  30556  n0nsnel  32608  creq0  32832  axregs  35323  onvf1odlem1  35325  dftr6  35973  dfon3  36112  dffun10  36134  brub  36176  bj-bixor  36824  bj-modal4e  36982  con2bii2  37615  heiborlem1  38091  heiborlem6  38096  heiborlem8  38098  cdleme0nex  40695  aks4d1p7  42482  wopprc  43416  n0nsn2el  47414  1nevenALTV  48080  resinsnALT  49261