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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xor3  384  imnan  401  annim  405  pm4.53  985  pm4.55  987  oran  989  nanan  1492  xnor  1512  xorneg  1523  noror  1535  alnex  1784  exnal  1830  exnalimn  1847  2exnexn  1849  nne  2945  dfrex2  3074  rexnal  3101  r2exlem  3144  ddif  4136  dfun2  4259  dfin2  4260  difin  4261  disj4  4458  snnzb  4722  eqsnuniex  5359  onuninsuci  7826  poxp2  8126  frxp3  8134  omopthi  8657  dif1enlem  9153  dif1enlemOLD  9154  dfsup2  9436  rankxplim3  9873  alephgeom  10074  fin1a2lem7  10398  fin41  10436  reclem2pr  11040  1re  11211  ltnlei  11332  divalglem8  16340  f1omvdco3  19312  elcls  22569  ist1-2  22843  fin1aufil  23428  dchrelbas3  26731  sltval2  27149  sltres  27155  nosepeq  27178  nolt02o  27188  nogt01o  27189  nosupbnd2lem1  27208  noinfbnd2lem1  27223  madebdaylemlrcut  27383  tgdim01  27748  axcontlem12  28223  avril1  29706  creq0  31948  dftr6  34710  dfon3  34853  dffun10  34875  brub  34915  bj-bixor  35458  bj-modal4e  35582  con2bii2  36203  heiborlem1  36668  heiborlem6  36673  heiborlem8  36675  cdleme0nex  39150  aks4d1p7  40937  wopprc  41755  n0nsn2el  45722  1nevenALTV  46346